operator_norm): split a proof (#11112)

Commit

4 years ago

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

Author

urkud

Parents

11de8674

mathlib f6d0f8d1 - refactor(analysis/normed_space/operator_norm): split a proof (#11112)

mathlib
f6d0f8d1 - refactor(analysis/normed_space/operator_norm): split a proof (#11112)