no goals
ι : Type ?u.578469
𝕜 : Type ?u.578472
E : Type u_1
F : Type ?u.578478
A : Type ?u.578481
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f [[a, b]]
rw [intervalIntegrable_iff, ← Icc_min_max, uIoc, integrableOn_Icc_iff_integrableOn_Ioc]