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.
- edges : set (sym2 V)
- sub_edges : self.edges ⊆ G.edge_set
- disjoint : ∀ (x y : sym2 V), x ∈ self.edges → y ∈ self.edges → ∀ (v : V), v ∈ x ∧ v ∈ y → x = y
A matching on
G is a subset of its edges such that no two edges share a vertex.