ι : Type ?u.6369999
𝕜 : Type ?u.6370002
E : Type ?u.6370005
F : Type ?u.6370008
A : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f✝ g✝ : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → A
hf : IntegrableOn f (Ι a b)
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn (fun x => f x * g x) (Ι a b)
ι : Type ?u.6369999
𝕜 : Type ?u.6370002
E : Type ?u.6370005
F : Type ?u.6370008
A : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f✝ g✝ : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → A
hf : IntervalIntegrable f μ a b
hg : ContinuousOn g [[a, b]]
⊢ IntervalIntegrable (fun x => f x * g x) μ a b
rw [intervalIntegrable_iff] at hf ⊢
no goals
ι : Type ?u.6369999
𝕜 : Type ?u.6370002
E : Type ?u.6370005
F : Type ?u.6370008
A : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f✝ g✝ : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → A
hf : IntegrableOn f (Ι a b)
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn (fun x => f x * g x) (Ι a b)
exact hf.mul_continuousOn_of_subset hg measurableSet_Ioc isCompact_uIcc Ioc_subset_Icc_self