Mathlib v3 is deprecated. Go to Mathlib v4

Theorem open_mapping_affine

Modification history

2022-01-08 18:36
src/analysis/normed_space/banach.lean
chore(analysis/normed_space/banach): move more to the `continuous_linear_map` NS (#11263) …
Deleted open_mapping_affineView on Github →
2021-10-06 15:46
src/analysis/normed_space/banach.lean
feat(analysis/normed_space/banach): open mapping theorem for maps between affine spaces (#9540) …
Added open_mapping_affineView on Github →