toColoring' — Mathlib

English

A coloring by sets of vertices given by P.partOfVertex, i.e., colors are blocks themselves (Set V).

Русский

Раскраска вершин графа, где цветами служат сами множества блоков разбиения.

LaTeX

$$toColoring' : G.Coloring (Set V)$$

Lean4

/-- Like `SimpleGraph.Partition.toColoring` but uses `Set V` as the coloring type. -/
def toColoring' : G.Coloring (Set V) :=
  Coloring.mk P.partOfVertex fun hvw ↦ P.partOfVertex_ne_of_adj hvw

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