no goals
α : Type u_1
β : Type ?u.4455149
E : Type u_2
F : Type ?u.4455155
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
inst✝ : NoAtoms μ
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ioo a b)
rw [integrableOn_Icc_iff_integrableOn_Ioc, integrableOn_Ioc_iff_integrableOn_Ioo]