Commit 2023-02-20 05:08 f2e96652

View on Github →

feat: Port Topology.IsLocallyHomeomorph (#2382) Renaming only.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/IsLocallyHomeomorph.lean

added theorem IsLocallyHomeomorph.map_nhds_eq

added theorem IsLocallyHomeomorph.mk

added def IsLocallyHomeomorph

added theorem IsLocallyHomeomorphOn.map_nhds_eq

added theorem IsLocallyHomeomorphOn.mk

added def IsLocallyHomeomorphOn

added theorem isLocallyHomeomorph_iff_isLocallyHomeomorphOn_univ