Theorems · Theorem · measure theory

intervalIntegral.continuous_primitive

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E}
  [MeasureTheory.NullSingletonClass μ],
  (∀ (a b : ℝ), IntervalIntegrable f μ a b) → ∀ (a : ℝ), Continuous fun b => ∫ (x : ℝ) in a..b, f x ∂μ

Defined in

Mathlib.MeasureTheory.Integral.DominatedConvergence

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceMeasureTheory.NullSingletonClass