α : Type u_1
β : Type u_2
γ : Type ?u.239415
δ : Type ?u.239418
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
hf : Tendsto (fun s => ∑ b in s, f b) atTop (𝓝 a)
hg : Tendsto (fun s => ∑ b in s, g b) atTop (𝓝 b)
⊢ Tendsto (fun s => ∑ b in s, (f b + g b)) atTop (𝓝 (a + b))
α : Type u_1
β : Type u_2
γ : Type ?u.239415
δ : Type ?u.239418
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
hf : HasSum f a
hg : HasSum g b
⊢ HasSum (fun b => f b + g b) (a + b)
dsimp only [HasSum] at hf hg ⊢
α : Type u_1
β : Type u_2
γ : Type ?u.239415
δ : Type ?u.239418
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
hf : Tendsto (fun s => ∑ b in s, f b) atTop (𝓝 a)
hg : Tendsto (fun s => ∑ b in s, g b) atTop (𝓝 b)
⊢ Tendsto (fun s => ∑ x in s, f x + ∑ x in s, g x) atTop (𝓝 (a + b))
α : Type u_1
β : Type u_2
γ : Type ?u.239415
δ : Type ?u.239418
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
hf : Tendsto (fun s => ∑ b in s, f b) atTop (𝓝 a)
hg : Tendsto (fun s => ∑ b in s, g b) atTop (𝓝 b)
⊢ Tendsto (fun s => ∑ b in s, (f b + g b)) atTop (𝓝 (a + b))
simp_rw [sum_add_distrib]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.239415
δ : Type ?u.239418
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
hf : Tendsto (fun s => ∑ b in s, f b) atTop (𝓝 a)
hg : Tendsto (fun s => ∑ b in s, g b) atTop (𝓝 b)
⊢ Tendsto (fun s => ∑ x in s, f x + ∑ x in s, g x) atTop (𝓝 (a + b))
exact hf.add hg