ι : Type ?u.10878693
𝕜 : Type ?u.10878696
E : Type u_1
F : Type ?u.10878702
A : Type ?u.10878705
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
h : ¬IntegrableOn f (Ι a b)
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = 0
ι : Type ?u.10878693
𝕜 : Type ?u.10878696
E : Type u_1
F : Type ?u.10878702
A : Type ?u.10878705
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
h : ¬IntervalIntegrable f μ a b
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = 0
rw [intervalIntegrable_iff] at h
no goals
ι : Type ?u.10878693
𝕜 : Type ?u.10878696
E : Type u_1
F : Type ?u.10878702
A : Type ?u.10878705
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
h : ¬IntegrableOn f (Ι a b)
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = 0
rw [intervalIntegral_eq_integral_uIoc, integral_undef h, smul_zero]