Commit 2025-07-01 11:28 3f037758

View on Github →

chore: reorder arguments in pathComponentIn (#26573) pathComponentIn x F and connectedComponentIn F x have opposite argument orders. I choose to reorder the arguments in pathComponentIn for no strong reason. Perhaps one can read, "the path component in F at x".

Estimated changes

modified theorem pathComponentIn_mem_nhds
modified theorem isPathConnected_iff_eq
modified theorem mem_pathComponentIn_self
modified def pathComponentIn
modified theorem pathComponentIn_congr
modified theorem pathComponentIn_subset
modified theorem pathComponentIn_univ