∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b₀ b₁ b₂ : ℝ} {μ : MeasureTheory.Measure ℝ}
  {f : ℝ → E},
  μ {b₀} = 0 →
    IntervalIntegrable f μ (min a b₁) (max a b₂) →
      ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Set.Icc b₁ b₂) b₀