Theorems · Theorem · measure theory

intervalIntegral.integral_mono_on_of_le_Ioo

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

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

MeasureTheory.NullSingletonClass