chromaticNumber_le_sum_right

Mathlib.Combinatorics.SimpleGraph.Sum

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

English

The chromatic number of H does not exceed the chromatic number of the sum G ⊕g H.

Русский

Хроматическое число H не превосходит хроматическое число суммы G ⊕g H.

LaTeX

$$$ H.chromaticNumber \le (G \oplus_g H).chromaticNumber $$$

Lean4

theorem chromaticNumber_le_sum_right : H.chromaticNumber ≤ (G ⊕g H).chromaticNumber :=
  chromaticNumber_le_of_forall_imp (fun _ h ↦ h.of_sum_right)

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

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

Разделы

Аффилиация

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