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

SimpleGraph.Subgraph.IsMatching
:M.IsMatching
means thatM
is a matching of its underlying graph. denotedM.is_matching
. 
SimpleGraph.Subgraph.IsPerfectMatching
defines when a subgraphM
of a simple graph is a perfect matching, denotedM.IsPerfectMatching
.
TODO #

Define an
other
function and prove useful results about it (https://leanprover.zulipchat.com/#narrow/stream/252551graphtheory/topic/matchings/near/266205863) 
Provide a bicoloring for matchings (https://leanprover.zulipchat.com/#narrow/stream/252551graphtheory/topic/matchings/near/265495120)

Tutte's Theorem

Hall's Marriage Theorem (see combinatorics.hall)
The subgraph M
of G
is a matching if every vertex of M
is incident to exactly one edge in M
.
We say that the vertices in M.support
are matched or saturated.
Equations
 SimpleGraph.Subgraph.IsMatching M = ∀ ⦃v : V⦄, v ∈ M.verts → ∃! w : V, M.Adj v w
Instances For
Given a vertex, returns the unique edge of the matching it is incident to.
Equations
 SimpleGraph.Subgraph.IsMatching.toEdge h v = { val := s(↑v, Exists.choose ⋯), property := ⋯ }
Instances For
The subgraph M
of G
is a perfect matching on G
if it's a matching and every vertex G
is
matched.