mathlib documentation

combinatorics.simple_graph.matching

Matchings #

Main definitions #

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.

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