English
If π1 and π2 are disjoint unions, the integral sum equals the sum of the two integral sums.
Русский
Если π1 и π2 — непрерывные объединения без пересечения, сумма интеграла равна сумме двух сумм.
LaTeX
$$$\forall π_1, π_2, (π_1.iUnion \cap π_2.iUnion) = \emptyset \Rightarrow \mathrm{integralSum} f vol (π_1.disjUnion π_2 h) = \mathrm{integralSum} f vol π_1 + \mathrm{integralSum} f vol π_2$$$
Lean4
@[simp]
theorem integralSum_disjUnion (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) {π₁ π₂ : TaggedPrepartition I}
(h : Disjoint π₁.iUnion π₂.iUnion) :
integralSum f vol (π₁.disjUnion π₂ h) = integralSum f vol π₁ + integralSum f vol π₂ :=
by
refine
(Prepartition.sum_disj_union_boxes h _).trans
(congr_arg₂ (· + ·) (sum_congr rfl fun J hJ => ?_) (sum_congr rfl fun J hJ => ?_))
· rw [disjUnion_tag_of_mem_left _ hJ]
· rw [disjUnion_tag_of_mem_right _ hJ]
