X : Type u_1
Y : Type ?u.2500484
E : Type u_3
R : Type ?u.2500490
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
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SecondCountableTopologyEither X 𝕜
inst✝ : NormedSpace 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsOpen s
hf : ∀ (k : Set X), k ⊆ s → IsCompact k → IntegrableOn f k
hg : ContinuousOn g s
⊢ ∀ (k : Set X), k ⊆ s → IsCompact k → IntegrableOn (fun x => g x • f x) k
X : Type u_1
Y : Type ?u.2500484
E : Type u_3
R : Type ?u.2500490
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
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SecondCountableTopologyEither X 𝕜
inst✝ : NormedSpace 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsOpen s
hf : LocallyIntegrableOn f s
hg : ContinuousOn g s
⊢ LocallyIntegrableOn (fun x => g x • f x) s
rw [MeasureTheory.locallyIntegrableOn_iff (Or.inr hs)] at hf⊢
no goals
X : Type u_1
Y : Type ?u.2500484
E : Type u_3
R : Type ?u.2500490
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
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SecondCountableTopologyEither X 𝕜
inst✝ : NormedSpace 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsOpen s
hf : ∀ (k : Set X), k ⊆ s → IsCompact k → IntegrableOn f k
hg : ContinuousOn g s
⊢ ∀ (k : Set X), k ⊆ s → IsCompact k → IntegrableOn (fun x => g x • f x) k
exact fun k hk_sub hk_c => (hf k hk_sub hk_c).continuousOn_smul (hg.mono hk_sub) hk_c