sum_disj_union_boxes — Mathlib

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

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