Theorems · Theorem · measure theory

MeasureTheory.setIntegral_trim

∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {X : Type u_5} {m m0 : MeasurableSpace X}
  {μ : MeasureTheory.Measure X} (hm : m ≤ m0) {f : X → E},
  MeasureTheory.StronglyMeasurable f →
    ∀ {s : Set X}, MeasurableSet s → ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, f x ∂μ.trim hm

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace