no goals
ι : Type ?u.927792
𝕜 : Type ?u.927795
E : Type u_1
F : Type ?u.927801
A : Type ?u.927804
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
c : E
⊢ IntervalIntegrable (fun x => c) μ a b ↔ c = 0 ∨ ↑↑μ (Ι a b) < ⊤
simp only [intervalIntegrable_iff, integrableOn_const]