mono — Mathlib

English

If the vertex set is odd, the empty graph is a Tutte violator for the empty set.

Русский

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

LaTeX

$$If Odd(n), then IsTutteViolator for ∅$$

Lean4

theorem mono {u : Set V} (h : G ≤ G') (ht : G'.IsTutteViolator u) : G.IsTutteViolator u :=
  by
  simp only [IsTutteViolator, Subgraph.induce_verts, Subgraph.verts_top] at *
  have := ncard_oddComponents_mono _ (Subgraph.deleteVerts_mono' (G := G) (G' := G') u h)
  simp only [oddComponents] at *
  cutsat

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