no goals
ι : Type ?u.19335522
𝕜 : Type ?u.19335525
E : Type ?u.19335528
F : Type ?u.19335531
A : Type ?u.19335534
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc a b)] f
hfi : IntervalIntegrable f μ a b
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = 0 ↔ f =ᵐ[Measure.restrict μ (Ioc a b)] 0
rw [integral_of_le hab, integral_eq_zero_iff_of_nonneg_ae hf hfi.1]