Commit 2023-10-21 06:49 ed50feef

View on Github →

feat: miscellaneous lemmas about local homeomorphisms (#7655)

Estimated changes

Modified Mathlib/Topology/IsLocallyHomeomorph.lean

added theorem IsLocallyHomeomorph.isTopologicalBasis

added theorem IsLocallyHomeomorph.of_comp

added theorem IsLocallyHomeomorph.openEmbedding_of_comp

added theorem IsLocallyHomeomorph.openEmbedding_of_injective

added theorem IsLocallyHomeomorphOn.mono

added theorem IsLocallyHomeomorphOn.of_comp_left

added theorem IsLocallyHomeomorphOn.of_comp_right

added theorem OpenEmbedding.isLocallyHomeomorph

added theorem isLocallyHomeomorphOn_iff_openEmbedding_restrict

added theorem isLocallyHomeomorph_homeomorph

added theorem isLocallyHomeomorph_iff_openEmbedding_restrict

Modified Mathlib/Topology/LocalHomeomorph.lean

added theorem LocalHomeomorph.openEmbedding_restrict

modified theorem LocalHomeomorph.to_openEmbedding