IsTutteViolator — Mathlib

English

If G ≤ G' and G' is a Tutte violator for a set u, then G is also a Tutte violator for u.

Русский

Если G ≤ G' и G' является нарушителем условия Тутта для множества u, то G тоже нарушитель условия Тутта для u.

LaTeX

$$$G\le G' \Rightarrow (G'.IsTutteViolator\ u)\Rightarrow (G.IsTutteViolator\ u)$$$

Lean4

/-- A set certifying non-existence of a perfect matching -/
def IsTutteViolator (G : SimpleGraph V) (u : Set V) : Prop :=
  u.ncard < ((⊤ : G.Subgraph).deleteVerts u).coe.oddComponents.ncard

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