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 ofV
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.
@[instance]
A perfect matching M
on graph G
is a matching such that
every vertex is contained in an edge of M
.
Equations
- M.is_perfect = (M.support = set.univ)