toColoring — Mathlib

English

From colorability with n colors and a bound n ≤ card α, one can construct a coloring C : G.Coloring α.

Русский

Из цветности с n цветами и ограничением n ≤ |α| можно получить раскраску C : G.Coloring α.

LaTeX

$$$G.Colorable n \\rightarrow (n \\le |\\alpha|) \\rightarrow \\exists C : G.Coloring(\\alpha)$$$

Lean4

/-- Noncomputably get a coloring from colorability. -/
noncomputable def toColoring [Fintype α] {n : ℕ} (hc : G.Colorable n) (hn : n ≤ Fintype.card α) : G.Coloring α :=
  by
  rw [← Fintype.card_fin n] at hn
  exact G.recolorOfCardLE hn hc.some

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