Theorem mem_pathComponentIn_self

Modification history

2025-07-01 11:28

Mathlib/Topology/Connected/PathConnected.lean

chore: reorder arguments in `pathComponentIn` (#26573) …

Modified mem_pathComponentIn_self View on Github →

2024-10-18 21:51

Mathlib/Topology/Connected/PathConnected.lean

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

Added mem_pathComponentIn_self View on Github →