Theorems · Theorem · measure theory

MeasureTheory.Integrable.continuous_primitive

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

Defined in

Mathlib.MeasureTheory.Integral.DominatedConvergence

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceMeasureTheory.NullSingletonClass