Theorem pathComponent_eq_connectedComponent

Modification history

2024-10-18 05:56
Mathlib/Topology/Connected/PathConnected.lean
feat(PathConnected): review API, add missing lemmas (#17855)
Added pathComponent_eq_connectedComponentView on Github →