Theorems · Theorem · measure theory

intervalIntegral.integral_mono_ae

∀ {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b →
    IntervalIntegrable f μ a b →
      IntervalIntegrable g μ a b → f ≤ᵐ[μ] g → ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

1 results in Mathlib

Foundations

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