Theorems · Theorem · real analysis

BoxIntegral.Prepartition.sum_biUnion_boxes

∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {M : Type u_2} [inst : AddCommMonoid M] (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (f : BoxIntegral.Box ι → M),
  ∑ J ∈ π.boxes.biUnion fun J => (πi J).boxes, f J = ∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J'

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Basic

Cited by

3 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoid