isEmpty_of_chromaticNumber_eq_zero

Mathlib.Combinatorics.SimpleGraph.Coloring

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

← MathLib Explorer

English

If the chromatic number is zero, then the vertex set is empty, and conversely.

Русский

Если χ(G)=0, то множество вершин пусто, и наоборот.

LaTeX

$$$G.chromaticNumber = 0 \\Rightarrow IsEmpty V$$$

Lean4

theorem isEmpty_of_chromaticNumber_eq_zero (h : G.chromaticNumber = 0) : IsEmpty V :=
  by
  have := colorable_of_chromaticNumber_ne_top (h ▸ ENat.zero_ne_top)
  rw [h] at this
  exact G.isEmpty_of_colorable_zero this

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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