Theorems · Theorem · measure theory

intervalIntegral.integral_mono_on

∀ {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b →
    IntervalIntegrable f μ a b →
      IntervalIntegrable g μ a b →
        (∀ x ∈ Set.Icc 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

5 results in Mathlib

Foundations

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