Theorems · Theorem · measure theory

intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt

∀ {f g : ℝ → ℝ} {a b : ℝ},
  a < b →
    ContinuousOn f (Set.Icc a b) →
      ContinuousOn g (Set.Icc a b) →
        (∀ x ∈ Set.Ioc a b, f x ≤ g x) →
          (∃ c ∈ Set.Icc a b, f c < g c) → ∫ (x : ℝ) in a..b, f x < ∫ (x : ℝ) in a..b, g x

If f and g are continuous on [a, b], a < b, f x ≤ g x on this interval, and f c < g c at some point c ∈ [a, b], then ∫ x in a..b, f x < ∫ x in a..b, g x.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

2 results in Mathlib

Foundations

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