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⟩