# mathlibdocumentation

combinatorics.simple_graph.matching

# 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:

TODO: Tutte and Hall require a definition of subgraphs.

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

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) :
set V

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