Commit 2025-11-04 18:11 fa060741

View on Github →

feat(Topology/Connected/LocPathConnected): convenience lemma for LocPathConnected + ConnectedSpace → PathConnectedSpace (#30315)

Estimated changes

Modified Mathlib/Topology/Connected/LocPathConnected.lean

added theorem PathConnectedSpace.of_locPathConnectedSpace

modified theorem pathConnectedSpace_iff_connectedSpace