English
Let G and H be simple graphs. If G is colorable with Fin n colors and H is colorable with Fin m colors, then the disjoint sum G ⊕g H is colorable with Fin max(n, m) colors.
Русский
Пусть G и H — простые графы. Если 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
/-- Color `G ⊕g H` with `Fin (n + m)` given a coloring of `G` with `Fin n` and a coloring of `H`
with `Fin m` -/
def sumFin {n m : ℕ} (cG : G.Coloring (Fin n)) (cH : H.Coloring (Fin m)) : (G ⊕g H).Coloring (Fin (max n m)) :=
sum (G.recolorOfEmbedding (Fin.castLEEmb (n.le_max_left m)) cG)
(H.recolorOfEmbedding (Fin.castLEEmb (n.le_max_right m)) cH)
