Commit 2022-01-08 18:36 09f69890
View on Github →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
.