sum_sumLeft_sumRight — Mathlib

English

For a coloring c of the disjoint sum G ⊕g H, applying sumLeft and then sumRight returns the original coloring c.

Русский

Для раскраски c графа G ⊕g H применение sumLeft затем sumRight возвращает исходную раскраску c.

LaTeX

$$$\\text{SimpleGraph.Coloring}.sumSumLeftSumRight(c) : c.sumLeft.sum c.sumRight = c$$$

Lean4

@[simp]
theorem sum_sumLeft_sumRight (c : (G ⊕g H).Coloring γ) : c.sumLeft.sum c.sumRight = c := by ext (u | u) <;> rfl

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