Commit 2025-03-19 09:47 9994bf5c

View on Github →

feat: the homotopy lifting property for covering maps (#22649)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

Modified Mathlib/Topology/Homotopy/Basic.lean

added theorem ContinuousMap.HomotopicRel.comp_continuousMap

Created Mathlib/Topology/Homotopy/Lifting.lean

added theorem IsCoveringMap.eq_liftHomotopy_iff'

added theorem IsCoveringMap.eq_liftHomotopy_iff

added theorem IsCoveringMap.eq_liftPath_iff'

added theorem IsCoveringMap.eq_liftPath_iff

added theorem IsCoveringMap.existsUnique_continuousMap_lifts

added theorem IsCoveringMap.exists_path_lifts

added theorem IsCoveringMap.homotopicRel_iff_comp

added theorem IsCoveringMap.injective_path_homotopic_mapFn

added theorem IsCoveringMap.liftHomotopy_lifts

added theorem IsCoveringMap.liftHomotopy_zero

added theorem IsCoveringMap.liftPath_apply_one_eq_of_homotopicRel

added theorem IsCoveringMap.liftPath_lifts

added theorem IsCoveringMap.liftPath_zero

added theorem IsLocalHomeomorph.continuous_lift

added theorem IsLocalHomeomorph.existsUnique_continuousMap_lifts

added theorem IsLocalHomeomorph.exists_lift_nhds

added theorem IsLocalHomeomorph.monodromy_theorem