colorClasses_finite

Mathlib.Combinatorics.SimpleGraph.Coloring

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

English

If α is finite, then the color classes are finite.

Русский

Если множество цветов α конечное, то множество цветовых классов конечное.

LaTeX

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

Lean4

theorem colorClasses_finite [Finite α] : C.colorClasses.Finite :=
  Setoid.finite_classes_ker _

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

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

Разделы

Аффилиация

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