Main definitions #
matchingon a simple graph is a subset of its edge set such that no two edges share an endpoint.
perfect_matchingon a simple graph is a matching in which every vertex belongs to an edge.
- Lemma stating that the existence of a perfect matching on
Gimplies that the cardinality of
Vis even (assuming it's finite)
- Hall's Marriage Theorem (see combinatorics.hall)
- Tutte's Theorem
- consider coercions instead of type definition for
- consider expressing
matching_vertsas union: https://github.com/leanprover-community/mathlib/pull/5156#discussion_r532906131
TODO: Tutte and Hall require a definition of subgraphs.