Commit 2023-12-11 18:22 fe44d905

View on Github →

chore: rename IsLocallyHomeomorph{On} to IsLocalHomeomorph{On} (#8983) This matches informal math terminology: IsLocallyHomeomorph f means "f is a local homeomorphism". zulip discussion

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Covering.lean

Renamed Mathlib/Topology/IsLocallyHomeomorph.lean to Mathlib/Topology/IsLocalHomeomorph.lean

added theorem Homeomorph.isLocalHomeomorph

deleted theorem Homeomorph.isLocallyHomeomorph

added theorem IsLocalHomeomorph.isLocallyInjective

added theorem IsLocalHomeomorph.isTopologicalBasis

added theorem IsLocalHomeomorph.map_nhds_eq

added theorem IsLocalHomeomorph.mk

added theorem IsLocalHomeomorph.of_comp

added theorem IsLocalHomeomorph.openEmbedding_of_comp

added theorem IsLocalHomeomorph.openEmbedding_of_injective

added def IsLocalHomeomorph

added theorem IsLocalHomeomorphOn.map_nhds_eq

added theorem IsLocalHomeomorphOn.mk

added theorem IsLocalHomeomorphOn.mono

added theorem IsLocalHomeomorphOn.of_comp_left

added theorem IsLocalHomeomorphOn.of_comp_right

added def IsLocalHomeomorphOn

deleted theorem IsLocallyHomeomorph.isLocallyInjective

deleted theorem IsLocallyHomeomorph.isTopologicalBasis

deleted theorem IsLocallyHomeomorph.map_nhds_eq

deleted theorem IsLocallyHomeomorph.mk

deleted theorem IsLocallyHomeomorph.of_comp

deleted theorem IsLocallyHomeomorph.openEmbedding_of_comp

deleted theorem IsLocallyHomeomorph.openEmbedding_of_injective

deleted def IsLocallyHomeomorph

deleted theorem IsLocallyHomeomorphOn.map_nhds_eq

deleted theorem IsLocallyHomeomorphOn.mk

deleted theorem IsLocallyHomeomorphOn.mono

deleted theorem IsLocallyHomeomorphOn.of_comp_left

deleted theorem IsLocallyHomeomorphOn.of_comp_right

deleted def IsLocallyHomeomorphOn

added theorem OpenEmbedding.isLocalHomeomorph

deleted theorem OpenEmbedding.isLocallyHomeomorph

added theorem isLocalHomeomorphOn_iff_openEmbedding_restrict

added theorem isLocalHomeomorph_iff_isLocalHomeomorphOn_univ

added theorem isLocalHomeomorph_iff_openEmbedding_restrict

deleted theorem isLocallyHomeomorphOn_iff_openEmbedding_restrict

deleted theorem isLocallyHomeomorph_iff_isLocallyHomeomorphOn_univ

deleted theorem isLocallyHomeomorph_iff_openEmbedding_restrict