no goals
α : Type u_1
β : Type u_2
γ : Type ?u.399252
δ : Type ?u.399255
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
hf : Summable fun b => -f b
⊢ Summable f
simpa only [neg_neg] using hf.neg