α : Type u_1
β : Type u_2
γ : Type ?u.401752
δ : Type ?u.401755
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
hf : HasSum f a₁
hg : HasSum g a₂
⊢ HasSum (fun b => f b + -g b) (a₁ + -a₂)
α : Type u_1
β : Type u_2
γ : Type ?u.401752
δ : Type ?u.401755
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
hf : HasSum f a₁
hg : HasSum g a₂
⊢ HasSum (fun b => f b - g b) (a₁ - a₂)
simp only [sub_eq_add_neg]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.401752
δ : Type ?u.401755
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
hf : HasSum f a₁
hg : HasSum g a₂
⊢ HasSum (fun b => f b + -g b) (a₁ + -a₂)
exact hf.add hg.neg