A matching for a simple graph is a set of disjoint pairs of adjacent vertices, and the set of all the vertices in a matching is called its support (and sometimes the vertices in the support are said to be saturated by the matching). A perfect matching is a matching whose support contains every vertex of the graph.
In this module, we represent a matching as a subgraph whose vertices are each incident to at most one edge, and the edges of the subgraph represent the paired vertices.
Main definitions #
Mis a matching of its underlying graph. denoted
simple_graph.subgraph.is_perfect_matchingdefines when a subgraph
Mof a simple graph is a perfect matching, denoted
otherfunction and prove useful results about it (https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/matchings/near/266205863)
Provide a bicoloring for matchings (https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/matchings/near/265495120)
Hall's Marriage Theorem (see combinatorics.hall)
G is a matching if every vertex of
M is incident to exactly one edge in
We say that the vertices in
M.support are matched or saturated.
Given a vertex, returns the unique edge of the matching it is incident to.
G is a perfect matching on
G if it's a matching and every vertex
- M.is_perfect_matching = (M.is_matching ∧ M.is_spanning)