∀ {ι : Type u_3} {M : Type u_7} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M]
  {f : ι → M}, (∀ (i : ι), 0 ≤ f i) → (∃ i, 0 < f i) → (Function.support f).Finite → 0 < ∑ᶠ (i : ι), f i