colorClasses_isPartition

Mathlib.Combinatorics.SimpleGraph.Coloring

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

English

For any coloring C, the collection of its color classes forms a partition of the vertex set: C.colorClasses partitions V.

Русский

Коллекция цветовых классов раскраски C образует разбиение множества вершин V.

LaTeX

$$$\\operatorname{IsPartition}(C.colorClasses)$$$

Lean4

theorem colorClasses_isPartition : Setoid.IsPartition C.colorClasses :=
  Setoid.isPartition_classes (Setoid.ker C)

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

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

Разделы

Аффилиация

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