sum_max — Mathlib

English

If G is n-colorable and H is m-colorable, then the disjoint sum G ⊕g H is max(n, m)-colorable.

Русский

Если G имеет окраску Fin n и H имеет окраску Fin m, то сумма G ⊕g H допускает окраску Fin max(n, m).

LaTeX

$$$ (G.Colorable n) \land (H.Colorable m) \Rightarrow (G \oplus_g H).Colorable (\max n m) $$$

Lean4

theorem sum_max {n m : ℕ} (hG : G.Colorable n) (hH : H.Colorable m) : (G ⊕g H).Colorable (max n m) :=
  Nonempty.intro (hG.some.sumFin hH.some)

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