English
Let G be a simple graph. Then G is n-colorable if and only if there exists a coloring of the vertices by natural numbers such that every vertex uses a color strictly less than n; equivalently, there is a coloring into the set {0,1,...,n−1}.
Русский
Пусть G — простой граф. Тогда G можно раскрасить в n цветов ровно тогда, когда существует раскраска вершин натуральными числами, при которой каждая вершина получает цвет меньше n; эквивалентно раскраске в множество {0,1,...,n−1}.
LaTeX
$$$G.Colorable n \\iff \\exists C : G.Coloring \\mathbb{N}, \\ \\forall v,\\ C(v) < n$$$
Lean4
theorem colorable_iff_exists_bdd_nat_coloring (n : ℕ) : G.Colorable n ↔ ∃ C : G.Coloring ℕ, ∀ v, C v < n :=
by
constructor
· rintro hc
have C : G.Coloring (Fin n) := hc.toColoring (by simp)
let f := Embedding.completeGraph (@Fin.valEmbedding n)
use f.toHom.comp C
intro v
exact Fin.is_lt (C.1 v)
· rintro ⟨C, Cf⟩
refine ⟨Coloring.mk ?_ ?_⟩
· exact fun v => ⟨C v, Cf v⟩
· rintro v w hvw
simp only [Fin.mk_eq_mk, Ne]
exact C.valid hvw
