Matchings #

Main definitions #

a matching on a simple graph is a subset of its edge set such that no two edges share an endpoint.
a perfect_matching on a simple graph is a matching in which every vertex belongs to an edge.

TODO:

Lemma stating that the existence of a perfect matching on G implies that the cardinality of V is even (assuming it's finite)
Hall's Marriage Theorem
Tutte's Theorem
consider coercions instead of type definition for matching: https://github.com/leanprover-community/mathlib/pull/5156#discussion_r532935457
consider expressing matching_verts as union: https://github.com/leanprover-community/mathlib/pull/5156#discussion_r532906131

TODO: Tutte and Hall require a definition of subgraphs.

structure simple_graph.matching {V : Type u} (G : simple_graph V) :

Type u

edges : set (sym2 V)
sub_edges : c.edges ⊆ G.edge_set
disjoint : ∀ (x y : sym2 V), x ∈ c.edges → y ∈ c.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.

@[instance]

def simple_graph.matching.inhabited {V : Type u} (G : simple_graph V) :

Equations

def simple_graph.matching.support {V : Type u} {G : simple_graph V} (M : G.matching) :

M.support is the set of vertices of G that are contained in some edge of matching M

Equations

def simple_graph.matching.is_perfect {V : Type u} {G : simple_graph V} (M : G.matching) :

Prop

A perfect matching M on graph G is a matching such that every vertex is contained in an edge of M.

Equations

theorem simple_graph.matching.is_perfect_iff {V : Type u} {G : simple_graph V} (M : G.matching) :

M.is_perfect ↔ ∀ (v : V), ∃ (e : sym2 V) (H : e ∈ M.edges), v ∈ e