English
If π1 and π2 are disjoint in iUnion, then the sum over the union of their boxes equals the sum of the two separate sums.
Русский
Если iUnion π1 и π2 несовместны, то сумма по объединению их коробок равна сумме двух отдельных сумм.
LaTeX
$$$ \sum J \in π_1.boxes \cup π_2.boxes\, f(J) = \left( \sum J \in π_1.boxes \; f(J) \right) + \left( \sum J \in π_2.boxes \; f(J) \right). $$$
Lean4
@[simp]
theorem sum_disj_union_boxes {M : Type*} [AddCommMonoid M] (h : Disjoint π₁.iUnion π₂.iUnion) (f : Box ι → M) :
∑ J ∈ π₁.boxes ∪ π₂.boxes, f J = (∑ J ∈ π₁.boxes, f J) + ∑ J ∈ π₂.boxes, f J :=
sum_union <| disjoint_boxes_of_disjoint_iUnion h