Theorems · Theorem · measure theory

MeasureTheory.integral_biUnion_finset

∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} (t : Finset ι) {s : ι → Set X},
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Function.onFun Disjoint s) →
      (∀ i ∈ t, MeasureTheory.IntegrableOn f (s i) μ) →
        ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace