no goals
ι : Type u_2
κ : Type ?u.15436
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : HasSum f a
i : ι
hb : ∀ (j : ι), j ≠ i → 0 ≤ f j
⊢ ∀ (i_1 : ι), ¬i_1 ∈ {i} → 0 ≤ f i_1
simpa