Commit 2026-06-25 12:42 23f4bd67

View on Github →

feat: local homeomorphisms are covering maps for compact domains (#41031)

Estimated changes

Modified Mathlib/Analysis/Complex/CoveringMap.lean

Modified Mathlib/Topology/Covering/Basic.lean

added theorem IsClosedMap.isCoveringMapOn_of_isLocalHomeomorphOn

deleted theorem IsClosedMap.isCoveringMapOn_of_openPartialHomeomorph

added theorem IsCoveringMapOn.of_isLocalHomeomorphOn

deleted theorem IsCoveringMapOn.of_openPartialHomeomorph

added theorem isLocalHomeomorph_iff_isCoveringMap