colorable_set_nonempty_of_colorable

English

If a graph is colorable in some n colors, then the set of natural numbers k for which the graph is colorable is nonempty; in particular, at least one such k exists (namely the given n).

Русский

Если граф можно окрасить в n цветов, то множество натуральных k, для которых граф можно окрасить, непусто; в частности, существует хотя бы одно такое k (например, n).

LaTeX

$$$G.Colorable n \\Rightarrow {k \\in \\mathbb{N} \\mid G.Colorable k} \\neq \\emptyset$$$

Lean4

theorem colorable_set_nonempty_of_colorable {n : ℕ} (hc : G.Colorable n) : {n : ℕ | G.Colorable n}.Nonempty :=
  ⟨n, hc⟩

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