Commit 2021-12-30 14:54 f6d0f8d1

View on Github →

refactor(analysis/normed_space/operator_norm): split a proof (#11112) Split the proof of continuous_linear_map.complete_space into reusable steps. Motivated by #9862

Estimated changes

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.lipschitz_apply

added def continuous_linear_map.of_mem_closure_image_coe_bounded

added def continuous_linear_map.of_tendsto_of_bounded_range

added theorem continuous_linear_map.tendsto_of_tendsto_pointwise_of_cauchy_seq