English
If V is finite, and M is a perfect matching in a subgraph of G, then the total number of vertices V is even.
Русский
Если V конечен и существует совершенное совпадение в некотором подграфе G, тогда число вершин V чётно.
LaTeX
$$Even(Fintype.card V)$$
Lean4
theorem even_card_of_isPerfectMatching [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (c : ConnectedComponent G)
(hM : M.IsPerfectMatching) : Even (Fintype.card c.supp) :=
by
#adaptation_note /-- https://github.com/leanprover/lean4/pull/5020
some instances that use the chain of coercions
`[SetLike X], X → Set α → Sort _` are
blocked by the discrimination tree. This can be fixed by redeclaring the instance for `X`
using the double coercion but the proper fix seems to avoid the double coercion. -/
letI : DecidablePred fun x ↦ x ∈ (M.induce c.supp).verts := fun a ↦ G.instDecidableMemSupp c a
simpa using (hM.induce_connectedComponent_isMatching c).even_card
