Commit 2021-10-06 15:46 0b356b00
View on Github →feat(analysis/normed_space/banach): open mapping theorem for maps between affine spaces (#9540) Formalized as part of the Sphere Eversion project.
feat(analysis/normed_space/banach): open mapping theorem for maps between affine spaces (#9540) Formalized as part of the Sphere Eversion project.