chromaticNumber_bddBelow — Mathlib

English

The chromatic number of G has a lower bound 0; in particular, the set of colorable n is bounded below by 0.

Русский

Хроматическое число графа G имеет нижнюю границу 0; множество colorable n ограничено снизу нулём.

LaTeX

$$$0 \\le n \\text{ for all } n \\text{ with } G.Colorable n$$$

Lean4

theorem chromaticNumber_bddBelow : BddBelow {n : ℕ | G.Colorable n} :=
  ⟨0, fun _ _ => zero_le _⟩

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