toColoring — Mathlib

English

There is a coloring of G by the colors P.parts, obtained by coloring each vertex by the part containing it; adjacent vertices have different colors.

Русский

Существует раскраска графа G в цвета множества частей P, где вершина окрашена своим блоком; смежные вершины получают разные цвета.

LaTeX

$$toColoring : G.Coloring P.parts$$

Lean4

/-- Create a coloring using the parts themselves as the colors.
Each vertex is colored by the part it's contained in. -/
def toColoring : G.Coloring P.parts :=
  Coloring.mk (fun v ↦ ⟨P.partOfVertex v, P.partOfVertex_mem v⟩) fun hvw ↦
    by
    rw [Ne, Subtype.mk_eq_mk]
    exact P.partOfVertex_ne_of_adj hvw

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