mathlib3
8dcce05f - feat(analysis/normed_space): open mapping (#900)

Commit

7 years ago

feat(analysis/normed_space): open mapping (#900) * The Banach open mapping theorem * improve comments * feat(analysis/normed_space): rebase, fix build

References

#900 - feat(analysis/normed_space): open mapping

Author

sgouezel

Committer

ChrisHughes24

Parents

00aaf05a

mathlib3 8dcce05f - feat(analysis/normed_space): open mapping (#900)

mathlib3
8dcce05f - feat(analysis/normed_space): open mapping (#900)