Theorems · Theorem · measure theory

intervalIntegral.intervalIntegral_pos_of_pos_on

∀ {f : ℝ → ℝ} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b → (∀ x ∈ Set.Ioo a b, 0 < f x) → a < b → 0 < ∫ (x : ℝ) in a..b, f x

If f : ℝ → ℝ is integrable on (a, b] for real numbers a < b, and positive on the interior of the interval, then its integral over a..b is strictly positive.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

1 results in Mathlib

Foundations

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