no goals
α : Type u_1
β : Type ?u.3533131
E : Type u_2
F : Type ?u.3533137
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hb : ↑↑μ {b} ≠ ⊤
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ioo a b)
rw [integrableOn_Icc_iff_integrableOn_Ioc' ha, integrableOn_Ioc_iff_integrableOn_Ioo' hb]