Commit 2023-11-07 13:32 a1f33eb2

View on Github →

feat: miscellaneous lemmas about local homeomorphisms (#8062)

variant of extend_left_inv', stated in terms of images (instead of point-wise)
variant of map_source', stated for images of subsets (instead of point-wise)
a local homeomorphism and its inverse are open on its source

Estimated changes

Modified Mathlib/Data/Set/Function.lean

added theorem Set.EqOn.image_eq_self

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

added theorem LocalHomeomorph.extend_left_inv'

Modified Mathlib/Logic/Equiv/LocalEquiv.lean

added theorem LocalEquiv.map_source''

Modified Mathlib/Topology/LocalHomeomorph.lean

added theorem LocalHomeomorph.isOpen_image_of_subset_source

added theorem LocalHomeomorph.isOpen_image_symm_of_subset_target

added theorem LocalHomeomorph.map_source''