Commit 2024-12-19 13:05 f00d276c

View on Github →

feat(Combinatorics/SimpleGraph): setup of universal vertices (#20023) Added the defintion of universalVerts and deleteUniversalVerts along with some initial results. This is in preparation for a proof of Tutte's theorem.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean

added theorem SimpleGraph.Subgraph.IsMatching.exists_of_universalVerts

added def SimpleGraph.deleteUniversalVerts

added theorem SimpleGraph.isClique_universalVerts

added def SimpleGraph.universalVerts

Modified Mathlib/Data/Set/Card.lean

added theorem Set.cast_ncard

Modified Mathlib/SetTheory/Cardinal/Finite.lean

added theorem Nat.cast_card