Colorable — Mathlib

English

G.Colorable n means there exists a coloring of G by Fin n, i.e., a coloring using at most n colors.

Русский

G.Colorable n означает существование раскраски графа G на Fin n, то есть раскраска, использующая не более n цветов.

LaTeX

$$$\\text{G.Colorable}(n) \\equiv \\exists C : G.Coloring(\\mathrm{Fin}(n)).$$$

Lean4

/-- Whether a graph can be colored by at most `n` colors. -/
def Colorable (n : ℕ) : Prop :=
  Nonempty (G.Coloring (Fin n))

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