mono_left — Mathlib

English

If G ≤ G' and G'.Colorable n holds, then G.Colorable n. This expresses monotonicity of colorability under graph inclusion.

Русский

Если граф G включается в граф G' и G' можно окрасить в n цветов, то и G можно окрасить в n цветов. Свойство монотонности окрашивания.

LaTeX

$$$G \\leq G' \\Rightarrow (G'.Colorable n \\Rightarrow G.Colorable n)$$$

Lean4

theorem mono_left {G' : SimpleGraph V} (h : G ≤ G') {n : ℕ} (hc : G'.Colorable n) : G.Colorable n :=
  ⟨hc.some.comp (.ofLE h)⟩

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