instFintypeColoring — Mathlib

English

If V and α are finite, then the type of colorings G.Coloring α is finite.

Русский

Если вершины графа V и множество цветов α конечны, то множество раскрасок G.Coloring α конечно.

LaTeX

$$$Fintype(G.Coloring\\, \\alpha)$$$

Lean4

noncomputable instance [Fintype V] [Fintype α] : Fintype (Coloring G α) := by
  classical
  change Fintype (RelHom G.Adj (completeGraph α).Adj)
  apply Fintype.ofInjective _ RelHom.coe_fn_injective

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