Theorem IsPathConnected.subset_pathComponentIn

Modification history

2024-10-18 21:51

Mathlib/Topology/Connected/PathConnected.lean

feat(Topology/Connected/PathConnected): some lemmas for `pathComponentIn` (#16983) …

Added IsPathConnected.subset_pathComponentIn View on Github →