English
Distributes a finite sum over a BiUnion of boxes: the sum over J in π.boxes.biUnion of (πi J).boxes equals the iterated sum over J in π.boxes of the sum over J' in (πi J).boxes.
Русский
Распространяется суммирование по BiUnion коробок: сумма по J в π.boxes.biUnion от (πi J).boxes равна поочередной сумме по J в π.boxes и по J' в (πi J).boxes.
LaTeX
$$$ \\sum_{J \\in π.boxes.biUnion (\\lambda J, (π_i J).boxes)} f(J) \\\\ = \\sum_{J \\in π.boxes} \\sum_{J' \\in (π_i J).boxes} f(J') $$$
Lean4
@[simp]
theorem sum_biUnion_boxes {M : Type*} [AddCommMonoid M] (π : Prepartition I) (πi : ∀ J, Prepartition J)
(f : Box ι → M) : (∑ J ∈ π.boxes.biUnion fun J => (πi J).boxes, f J) = ∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J' :=
by
refine Finset.sum_biUnion fun J₁ h₁ J₂ h₂ hne => Finset.disjoint_left.2 fun J' h₁' h₂' => ?_
exact hne (π.eq_of_le_of_le h₁ h₂ ((πi J₁).le_of_mem h₁') ((πi J₂).le_of_mem h₂'))
