no goals
ι : Type ?u.11229466
𝕜 : Type ?u.11229469
E : Type u_1
F : Type ?u.11229475
A : Type ?u.11229478
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
hf : ¬AEStronglyMeasurable f (Measure.restrict μ (Ι a b))
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = 0
rw [intervalIntegral_eq_integral_uIoc, integral_non_aestronglyMeasurable hf, smul_zero]