Commit 2026-06-21 18:23 9c27dca6

View on Github →

refactor(Topology): rename LocPathConnected (#40868) Rename LocPathConnected to LocallyPathConnected per discussion at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Rename.20.60.60.60LocPathConnectedSpace.60.60.60.3F/with/582824006

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/CStarAlgebra/Unitary/Connected.lean

Modified Mathlib/Analysis/Complex/BranchLogRoot.lean

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

deleted theorem ChartedSpace.locPathConnectedSpace

added theorem ChartedSpace.locallyPathConnectedSpace

Modified Mathlib/Geometry/Manifold/Instances/Real.lean

Modified Mathlib/Topology/Algebra/Module/LocallyConvex.lean

deleted theorem Convex.locPathConnectedSpace

added theorem Convex.locallyPathConnectedSpace

Modified Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean

Renamed Mathlib/Topology/Connected/LocPathConnected.lean to Mathlib/Topology/Connected/LocallyPathConnected.lean

deleted theorem IsOpen.locPathConnectedSpace

added theorem IsOpen.locallyPathConnectedSpace

deleted theorem LocPathConnectedSpace.coinduced

deleted theorem LocPathConnectedSpace.of_bases

added theorem LocallyPathConnectedSpace.coinduced

added theorem LocallyPathConnectedSpace.of_bases

deleted theorem PathConnectedSpace.of_locPathConnectedSpace

added theorem PathConnectedSpace.of_locallyPathConnectedSpace

deleted theorem Topology.IsOpenEmbedding.locPathConnectedSpace

added theorem Topology.IsOpenEmbedding.locallyPathConnectedSpace

deleted theorem Topology.IsQuotientMap.locPathConnectedSpace

added theorem Topology.IsQuotientMap.locallyPathConnectedSpace

deleted theorem locPathConnectedSpace_iff_isOpen_pathComponentIn

deleted theorem locPathConnectedSpace_iff_pathComponentIn_mem_nhds

added theorem locallyPathConnectedSpace_iff_isOpen_pathComponentIn

added theorem locallyPathConnectedSpace_iff_pathComponentIn_mem_nhds

Modified Mathlib/Topology/Connected/PathComponentOne.lean

Modified Mathlib/Topology/Homotopy/Lifting.lean

modified theorem IsCoveringMap.existsUnique_continuousMap_lifts

modified theorem IsLocalHomeomorph.existsUnique_continuousMap_lifts

Modified Mathlib/Topology/Homotopy/LocallyContractible.lean