mono

Mathlib.Combinatorics.SimpleGraph.Coloring

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Colorable.mono

English

If n ≤ m and G is n-colorable, then G is m-colorable.

Русский

Если n ≤ m и граф G можно окрасить в n цветов, то можно окрасить и в m цветов.

LaTeX

$$$n \\le m \\Rightarrow G.Colorable n \\Rightarrow G.Colorable m$$$

Lean4

theorem mono {n m : ℕ} (h : n ≤ m) (hc : G.Colorable n) : G.Colorable m :=
  ⟨G.recolorOfCardLE (by simp [h]) hc.some⟩

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

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

Разделы

Аффилиация

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