English
For a finite graph, either there is a perfect matching or there exists a Tutte violator; the two conditions are equivalent in the even-odd dichotomy.
Русский
Для конечного графа либо существует совершенное совпадение, либо существует нарушитель Тутты; два условия эквивалентны по четности/нечетности.
LaTeX
$$Exists M IsPerfectMatching ⇔ ∀ u, ¬IsTutteViolator u$$
Lean4
/-- Proves the necessity part of Tutte's theorem -/
theorem not_isTutteViolator_of_isPerfectMatching {M : Subgraph G} (hM : M.IsPerfectMatching) (u : Set V) :
¬G.IsTutteViolator u :=
by
choose f hf g hgf hg using ConnectedComponent.odd_matches_node_outside hM (u := u)
have hfinj : f.Injective := fun c d hcd ↦
by
replace hcd : g c = g d := Subtype.val_injective <| hM.1.eq_of_adj_right (hgf c) (hcd ▸ hgf d)
exact Subtype.val_injective <| ConnectedComponent.eq_of_common_vertex (hg c) (hcd ▸ hg d)
simpa [IsTutteViolator] using Nat.card_le_card_of_injective (fun c ↦ ⟨f c, hf c⟩) (fun c d ↦ by simp [hfinj.eq_iff])
