6.16. MappingDegree.ConnectedManifoldPathConnected🔗

Jacobians.MappingDegree.ConnectedManifoldPathConnected — source

pathConnectedSpace_of_connectedSpace_locPathConnected

Any topological space that is connected and locally path-connected is path-connected. This is exactly PathConnectedSpace.of_locPathConnectedSpace from mathlib, re-exported under a project-local name.

theorem pathConnectedSpace_of_connectedSpace_locPathConnected
    {Y : Type*} [TopologicalSpace Y] [ConnectedSpace Y] [LocPathConnectedSpace Y] :
    PathConnectedSpace Y