Theorems · Theorem · measure theory

Continuous.intervalIntegrable

∀ {E : Type u_5} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ]
  {u : ℝ → E}, Continuous u → ∀ (a b : ℝ), IntervalIntegrable u μ a b

A continuous function on ℝ is IntervalIntegrable with respect to any locally finite measure ν on ℝ.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

32 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupMeasureTheory.IsLocallyFiniteMeasure