chromaticNumber_le_sum_left

Mathlib.Combinatorics.SimpleGraph.Sum

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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