Theorem Homeomorph.locallyPathConnectedSpace

Modification history

2026-08-13 15:21

Mathlib/Topology/Connected/LocallyPathConnected.lean

feat(Topology/Connected): transport path-connectedness along homeomorphisms (#41665) …

Added Homeomorph.locallyPathConnectedSpace View on Github →