Theorems · Theorem · measure theory

MeasureTheory.Integrable.trim

∀ {α : Type u_1} {m : MeasurableSpace α} {H : Type u_8} [inst : NormedAddCommGroup H] {m0 : MeasurableSpace α}
  {μ' : MeasureTheory.Measure α} {f : α → H} (hm : m ≤ m0),
  MeasureTheory.Integrable f μ' → MeasureTheory.StronglyMeasurable f → MeasureTheory.Integrable f (μ'.trim hm)

Defined in

Mathlib.MeasureTheory.Function.L1Space.Integrable

Cited by

10 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup