colorable_of_isEmpty

Mathlib.Combinatorics.SimpleGraph.Coloring

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

English

If V is empty, then G is n-colorable for every n.

Русский

Если V пусто, то граф G цветоспособен при любом количестве цветов n.

LaTeX

$$$IsEmpty V \\Rightarrow G.Colorable n$$$

Lean4

theorem colorable_of_isEmpty [IsEmpty V] (n : ℕ) : G.Colorable n :=
  ⟨G.coloringOfIsEmpty⟩

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

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

Разделы

Аффилиация

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