colorable_of_fintype

Mathlib.Combinatorics.SimpleGraph.Coloring

URI: https://scilib.ai/kg/mathlib#SimpleGraph.colorable_of_fintype

English

If V is finite, then G is colorable with card(V) colors.

Русский

Если множество вершин V конечно, граф G можно раскрасить цветами из V количеством цветов Card(V).

LaTeX

$$$[Fintype V] \\Rightarrow G.Colorable (Fintype.card V)$$$

Lean4

theorem colorable_of_fintype (G : SimpleGraph V) [Fintype V] : G.Colorable (Fintype.card V) :=
  G.selfColoring.colorable

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

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

Разделы

Аффилиация

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