affine_isometry): affine maps are open iff their underlying linear maps are (#9538)

Commit

4 years ago

feat(analysis/normed_space/affine_isometry): affine maps are open iff their underlying linear maps are (#9538) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents

63903f27

mathlib 815eaca0 - feat(analysis/normed_space/affine_isometry): affine maps are open iff their underlying linear maps are (#9538)

mathlib
815eaca0 - feat(analysis/normed_space/affine_isometry): affine maps are open iff their underlying linear maps are (#9538)