X : Type u_1
Y : Type ?u.2499165
E : Type ?u.2499168
R : Type u_2
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : NormedAddCommGroup E
f✝ : X → E
μ : Measure X
s✝ : Set X
inst✝⁴ : OpensMeasurableSpace X
A K : Set X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : ∀ (k : Set X), k ⊆ s → IsCompact k → IntegrableOn f k
hg : ContinuousOn g s
hs : IsOpen s
⊢ ∀ (k : Set X), k ⊆ s → IsCompact k → IntegrableOn (fun x => f x * g x) k
X : Type u_1
Y : Type ?u.2499165
E : Type ?u.2499168
R : Type u_2
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : NormedAddCommGroup E
f✝ : X → E
μ : Measure X
s✝ : Set X
inst✝⁴ : OpensMeasurableSpace X
A K : Set X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : LocallyIntegrableOn f s
hg : ContinuousOn g s
hs : IsOpen s
⊢ LocallyIntegrableOn (fun x => f x * g x) s
rw [MeasureTheory.locallyIntegrableOn_iff (Or.inr hs)] at hf⊢
no goals
X : Type u_1
Y : Type ?u.2499165
E : Type ?u.2499168
R : Type u_2
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : NormedAddCommGroup E
f✝ : X → E
μ : Measure X
s✝ : Set X
inst✝⁴ : OpensMeasurableSpace X
A K : Set X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : ∀ (k : Set X), k ⊆ s → IsCompact k → IntegrableOn f k
hg : ContinuousOn g s
hs : IsOpen s
⊢ ∀ (k : Set X), k ⊆ s → IsCompact k → IntegrableOn (fun x => f x * g x) k
exact fun k hk_sub hk_c => (hf k hk_sub hk_c).mul_continuousOn (hg.mono hk_sub) hk_c