no goals
α : Type u_1
β : Type u_2
γ : Type ?u.690029
δ : Type ?u.690032
inst✝³ : AddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : CompleteSpace α
⊢ Summable f ↔ ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
rw [summable_iff_cauchySeq_finset, cauchySeq_finset_iff_vanishing]