colorable_sum — Mathlib

English

For every n, (G ⊕g H).Colorable n is equivalent to G.Colorable n and H.Colorable n.

Русский

Для каждого n равносильно: сумма G и H цветоспособна в n цветов тогда и только тогда обе части цветоспособны в n цветов.

LaTeX

$$$ (G \oplus_g H).Colorable n \iff G.Colorable n \land H.Colorable n $$$

Lean4

@[simp]
theorem colorable_sum {n : ℕ} : (G ⊕g H).Colorable n ↔ G.Colorable n ∧ H.Colorable n :=
  ⟨fun cGH => ⟨cGH.of_sum_left, cGH.of_sum_right⟩, fun ⟨cG, cH⟩ => by rw [← n.max_self]; exact cG.sum_max cH⟩

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