Theorems · Theorem · measure theory

MeasureTheory.integrable_of_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 (μ'.trim hm) → MeasureTheory.Integrable f μ'

Defined in

Mathlib.MeasureTheory.Function.L1Space.Integrable

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup