Theorems · Theorem · real analysis

BoxIntegral.integralSum_fiberwise

∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} {α : Type u_1}
  (g : BoxIntegral.Box ι → α) (f : (ι → ℝ) → E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤)
  (π : BoxIntegral.TaggedPrepartition I),
  ∑ y ∈ Finset.image g π.boxes, BoxIntegral.integralSum f vol (π.filter fun x => g x = y) =
    BoxIntegral.integralSum f vol π

Defined in

Mathlib.Analysis.BoxIntegral.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace