sum — Mathlib

English

Color the disjoint sum G ⊕g H by coloring G and H separately and combining the colorings.

Русский

Раскрасим дизъюнктное суммирование графов G ⊕g H, используя раскраски G и H по отдельности и объединяя их.

LaTeX

$$$\mathrm{sum}(c_G,c_H) : (G \oplus_g H).Coloring \gamma\;\text{where }\text{toFun} = \mathrm{Sum.elim}(c_G,c_H) \;\text{and }\text{map_rel}'$$$

Lean4

/-- Color `G ⊕g H` with colorings of `G` and `H` -/
def sum (cG : G.Coloring γ) (cH : H.Coloring γ) : (G ⊕g H).Coloring γ
    where
  toFun := Sum.elim cG cH
  map_rel' {u v} huv := by cases u <;> cases v <;> simp_all [cG.valid, cH.valid]

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