Commit 2025-02-10 10:42 db325194

View on Github →

feat(Combinatorics/SimpleGraph/Path): representatives of connected components (#20024) Add the concept of a set of representatives of a connected component along with some basic lemma's on it. In preparation for a proof of Tutte's theorem.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean

added theorem SimpleGraph.ConnectedComponent.Represents.disjoint_supp_of_not_mem

added theorem SimpleGraph.ConnectedComponent.Represents.existsUnique_rep

added theorem SimpleGraph.ConnectedComponent.Represents.image_out

added theorem SimpleGraph.ConnectedComponent.Represents.ncard_inter

added theorem SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_mem

added theorem SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_not_mem

added def SimpleGraph.ConnectedComponent.Represents