Theorems · Theorem · measure theory

MeasureTheory.integrable_of_le_of_le

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g₁ g₂ : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    g₁ ≤ᵐ[μ] f →
      f ≤ᵐ[μ] g₂ → MeasureTheory.Integrable g₁ μ → MeasureTheory.Integrable g₂ μ → MeasureTheory.Integrable f μ

Defined in

Mathlib.MeasureTheory.Function.L1Space.Integrable

Cited by

6 results in Mathlib

Foundations

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