Commit 2024-10-18 21:51 b9efa9d8

View on Github →

feat(Topology/Connected/PathConnected): some lemmas for pathComponentIn (#16983) Adds some basic lemmas about pathComponentIn, analogous to existing lemmas about pathComponent and connectedComponentIn.

Estimated changes

Modified Mathlib/Topology/Connected/PathConnected.lean

added theorem IsPathConnected.subset_pathComponentIn

added theorem isPathConnected_pathComponent

added theorem isPathConnected_pathComponentIn

added theorem mem_pathComponentIn_self

added theorem pathComponentIn_congr

added theorem pathComponentIn_mono

added theorem pathComponentIn_nonempty_iff

added theorem pathComponentIn_subset