empty — Mathlib

English

If a graph has no perfect matching and the number of vertices is even, there exists a Tutte violator.

Русский

Если граф не имеет совершенного совпадения, число вершин чётное, существует нарушитель Тутты.

LaTeX

$$$\exists u, G.IsTutteViolator\ u$$$

Lean4

theorem empty (hodd : Odd (Nat.card V)) : G.IsTutteViolator ∅ :=
  by
  rw [IsTutteViolator, Set.ncard_empty]
  exact ((odd_ncard_oddComponents _).mpr <| by simpa using hodd).pos

Похожие утверждения