colorClass

Mathlib.Combinatorics.SimpleGraph.Coloring

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Coloring.colorClass

English

The color class of a color c is the set of vertices colored by c.

Русский

Класс цвета c — это множество вершин, окрашенных в цвет c.

LaTeX

$$$\\mathrm{colorClass}(c) = \\{ v \\in V : C(v) = c \\}$$$

Lean4

/-- The color class of a given color.
-/
def colorClass (c : α) : Set V :=
  {v : V | C v = c}

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru