chromaticNumber_le_one_of_subsingleton

English

For any graph G, χ(G) ≠ ∞ if and only if there exists n with G.Colorable n.

Русский

Для любого графа G χ(G) конечно тогда и только тогда существует n, такое что G.Colorable n.

LaTeX

$$$G.chromaticNumber \\neq \\top \\iff \\exists n, G.Colorable n$$$

Lean4

theorem chromaticNumber_le_one_of_subsingleton (G : SimpleGraph V) [Subsingleton V] : G.chromaticNumber ≤ 1 :=
  by
  rw [← Nat.cast_one, chromaticNumber_le_iff_colorable]
  refine ⟨Coloring.mk (fun _ => 0) ?_⟩
  intro v w
  cases Subsingleton.elim v w
  simp

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