Theorems · Theorem · measure theory

intervalIntegral.integral_mono_interval

∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {c d : ℝ},
  c ≤ a →
    a ≤ b →
      b ≤ d →
        0 ≤ᵐ[μ.restrict (Set.Ioc c d)] f →
          IntervalIntegrable f μ c d → ∫ (x : ℝ) in a..b, f x ∂μ ≤ ∫ (x : ℝ) in c..d, f x ∂μ

Defined in: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 257 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
MeasureTheory.Measurestatement and proof · cited by 10,939
LE.le.transproof · cited by 3,151
MeasureTheory.aestatement and proof · cited by 2,352
MeasureTheory.integralproof · cited by 1,779
MeasureTheory.Measure.restrictstatement and proof · cited by 1,646
Set.Iocstatement and proof · cited by 971
intervalIntegralstatement and proof · cited by 546
Filter.EventuallyLEstatement and proof · cited by 383
IntervalIntegrablestatement and proof · cited by 316
intervalIntegral.integral_of_leproof · cited by 83
LE.le.eventuallyLEproof · cited by 21

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurableproof · cited by 1