no goals
ι : Type ?u.695028
𝕜 : Type ?u.695031
E : Type u_1
F : Type ?u.695037
A : Type ?u.695040
inst✝¹ : NormedAddCommGroup E
f✝ : ℝ → E
a✝ b✝ : ℝ
μ✝ : MeasureTheory.Measure ℝ
f : ℝ → E
a b : ℝ
hab : a ≤ b
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Icc a b)
rw [intervalIntegrable_iff_integrable_Ioc_of_le hab, integrableOn_Icc_iff_integrableOn_Ioc]