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