α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
γ : Type u_1
inst✝² : LocallyCompactSpace α
inst✝¹ : AddCommMonoid β
inst✝ : ContinuousAdd β
f : γ → C(α, β)
g : C(α, β)
hf : HasSum f g
x : α
evₓ : C(α, β) →+ β := AddMonoidHom.comp (Pi.evalAddMonoidHom (fun a => β) x) coeFnAddMonoidHom
⊢ HasSum (fun i => ↑(f i) x) (↑g x)
α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
γ : Type u_1
inst✝² : LocallyCompactSpace α
inst✝¹ : AddCommMonoid β
inst✝ : ContinuousAdd β
f : γ → C(α, β)
g : C(α, β)
hf : HasSum f g
x : α
⊢ HasSum (fun i => ↑(f i) x) (↑g x)
let evₓ : AddMonoidHom C(α, β) β := (Pi.evalAddMonoidHom _ x).comp coeFnAddMonoidHom
no goals
α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
γ : Type u_1
inst✝² : LocallyCompactSpace α
inst✝¹ : AddCommMonoid β
inst✝ : ContinuousAdd β
f : γ → C(α, β)
g : C(α, β)
hf : HasSum f g
x : α
evₓ : C(α, β) →+ β := AddMonoidHom.comp (Pi.evalAddMonoidHom (fun a => β) x) coeFnAddMonoidHom
⊢ HasSum (fun i => ↑(f i) x) (↑g x)
exact hf.map evₓ (ContinuousMap.continuous_eval_const' x)