no goals
ι : Type u_2
α : Type ?u.2223
E : Type u_1
F : Type ?u.2229
inst✝² : SeminormedAddCommGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : CompleteSpace E
f : ι → E
⊢ Summable f ↔ ∀ (ε : ℝ), ε > 0 → ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε
rw [summable_iff_cauchySeq_finset, cauchySeq_finset_iff_vanishing_norm]