no goals
ι : Type ?u.231038
𝕜 : Type ?u.231041
E : Type u_1
F : Type ?u.231047
A : Type ?u.231050
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ι a b)
rw [uIoc_eq_union, integrableOn_union, IntervalIntegrable]