2025-11-04 18:11
Mathlib/Topology/Connected/LocPathConnected.lean
feat(Topology/Connected/LocPathConnected): convenience lemma for `LocPathConnected` + `ConnectedSpace` → `PathConnectedSpace` (#30315)
Added PathConnectedSpace.of_locPathConnectedSpace