inverse): a map that has an invertible strict derivative at every point is an open map (#5753)

Commit

5 years ago

feat(analysis/calculus/inverse): a map that has an invertible strict derivative at every point is an open map (#5753) More generally, the same is true for a map that is a local homeomorphism near every point.

Author

urkud

Parents

4c1d12f5

mathlib3 ed0ae3e7 - feat(analysis/calculus/inverse): a map that has an invertible strict derivative at every point is an open map (#5753)

mathlib3
ed0ae3e7 - feat(analysis/calculus/inverse): a map that has an invertible strict derivative at every point is an open map (#5753)