English
If a finite graph has a perfect matching, then the total number of vertices is even; equivalently, each component contributes an even count.
Русский
Если в конечном графе есть совершенное совпадение, то общее число вершин чётно; каждый компонент вносит вклад чётного числа вершин.
LaTeX
$$Even(Fintype.card V)$$
Lean4
/-- A graph `G` consists of a set of cycles, if each vertex is either isolated or connected to
exactly two vertices. This is used to create new matchings by taking the `symmDiff` with cycles.
The definition of `symmDiff` that makes sense is the one for `SimpleGraph`. The `symmDiff`
for `SimpleGraph.Subgraph` deriving from the lattice structure also affects the vertices included,
which we do not want in this case. This is why this property is defined for `SimpleGraph`, rather
than `SimpleGraph.Subgraph`.
-/
def IsCycles (G : SimpleGraph V) :=
∀ ⦃v⦄, (G.neighborSet v).Nonempty → (G.neighborSet v).ncard = 2
