mathlib3

09f69890 - chore(analysis/normed_space/banach): move more to the `continuous_linear_map` NS (#11263)

chore(analysis/normed_space/banach): move more to the `continuous_linear_map` NS (#11263) ## Rename * `open_mapping` → `continuous_linear_map.is_open_map`; * `open_mapping_affine` → `affine_map.is_open_map`; ### New lemmas * `continuous_linear_map.quotient_map`, * `continuous_linear_map.interior_preimage`, * `continuous_linear_map.closure_preimage`, * `continuous_linear_map.frontier_preimage`.