Theorems · Theorem · measure theory

MeasureTheory.IntegrableOn.continuousWithinAt_Iic_primitive_Iio

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E}
  {a₀ : ℝ},
  MeasureTheory.IntegrableOn f (Set.Iio a₀) μ →
    ContinuousWithinAt (fun b => ∫ (x : ℝ) in Set.Iio b, f x ∂μ) (Set.Iic a₀) a₀

Defined in

Mathlib.MeasureTheory.Integral.DominatedConvergence

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace