English
The Finset of 3-cliques in graph t equals the image of t under toTriangle.
Русский
Финсет 3-клик графа t равен изображению t под toTriangle.
LaTeX
$$$ (graph\ t).cliqueFinset\ 3 = Finset.image\ toTriangle\ t $$$
Lean4
/-- **Tutte's theorem**
A graph has a perfect matching if and only if: For every subset `u` of vertices, removing this
subset induces at most `u.ncard` components of odd size. This is formally stated using the
predicate `IsTutteViolator`, which is satisfied exactly when this condition does not hold. -/
theorem tutte : (∃ M : Subgraph G, M.IsPerfectMatching) ↔ ∀ u, ¬G.IsTutteViolator u := by
classical
refine ⟨by rintro ⟨M, hM⟩; apply not_isTutteViolator_of_isPerfectMatching hM, ?_⟩
contrapose!
intro h
by_cases hvOdd : Odd (Nat.card V)
· exact ⟨∅, .empty hvOdd⟩
· exact exists_isTutteViolator h (Nat.not_odd_iff_even.mp hvOdd)
