bicoloring

Mathlib.Combinatorics.SimpleGraph.ConcreteColorings

URI: https://scilib.ai/kg/mathlib#SimpleGraph.pathGraph.bicoloring

← MathLib Explorer

English

The path graph P_n has chromatic number 2 for n ≥ 2.

Русский

Путь графа P_n имеет хроматическое число 2 при n ≥ 2.

LaTeX

$$(pathGraph n).chromaticNumber = 2$$

Lean4

/-- Bicoloring of a path graph -/
def bicoloring (n : ℕ) : Coloring (pathGraph n) Bool :=
  Coloring.mk (fun u ↦ u.val % 2 = 0) <| by
    intro u v
    rw [pathGraph_adj]
    rintro (h | h) <;> simp [← h, not_iff, Nat.succ_mod_two_eq_zero_iff]

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

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

Разделы

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

Аффилиация

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