Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-12-15 21:03
2d8f9a91
View on Github →
feat(Topology): IsCoveringMapOn ↔ IsCoveringMap restrictPreimage (
#27197
)
Estimated changes
Modified
Mathlib/Topology/Covering/Basic.lean
added
theorem
IsCoveringMap.comp_homeomorph
added
theorem
IsCoveringMap.comp_homeomorph_iff
added
theorem
IsCoveringMap.homeomorph_comp
added
theorem
IsCoveringMap.homeomorph_comp_iff
added
theorem
IsCoveringMap.restrictPreimage
added
theorem
IsCoveringMapOn.comp_homeomorph
added
theorem
IsCoveringMapOn.comp_homeomorph_iff
added
theorem
IsCoveringMapOn.homeomorph_comp
added
theorem
IsCoveringMapOn.homeomorph_comp_iff
added
theorem
IsCoveringMapOn.isCoveringMap_restrictPreimage
added
theorem
IsCoveringMapOn.of_isCoveringMap_restrictPreimage
added
theorem
IsCoveringMapOn.restrictPreimage
added
theorem
IsEvenlyCovered.comp_homeomorph
added
theorem
IsEvenlyCovered.comp_homeomorph_iff
added
theorem
IsEvenlyCovered.comp_subtypeVal
added
theorem
IsEvenlyCovered.homeomorph_comp
added
theorem
IsEvenlyCovered.homeomorph_comp_iff
added
theorem
IsEvenlyCovered.restrictPreimage
added
theorem
IsEvenlyCovered.subtypeVal_comp
modified
theorem
isCoveringMap_iff_isCoveringMapOn_univ