Commit 2026-08-13 15:21 652d7e3b

View on Github →

feat(Topology/Connected): transport path-connectedness along homeomorphisms (#41665) Add Homeomorph.pathConnectedSpace, Homeomorph.locallyPathConnectedSpace and Homeomorph.image_pathComponent, completing the family alongside the existing Homeomorph.connectedSpace and Homeomorph.locallyConnectedSpace.

Estimated changes

Modified Mathlib/Topology/Connected/LocallyPathConnected.lean

added theorem Homeomorph.locallyPathConnectedSpace

Modified Mathlib/Topology/Connected/PathConnected.lean

added theorem Continuous.image_pathComponent_subset

added theorem Continuous.mapsTo_pathComponent

added theorem Homeomorph.image_pathComponent

added theorem Homeomorph.pathConnectedSpace

added theorem Homeomorph.preimage_pathComponent

modified theorem JoinedIn.map

deleted theorem JoinedIn.map_continuousOn