Summation in topological groups

Remarks

Equivalently, the net $(s_F)$, indexed by the finite subsets of $I$ ordered by inclusion, converges to $s$. If $G$ is Hausdorff, a family has at most one sum; in Mathlib this is HasSum.unique. The definition does not use any order on $I$, so a bijection $\sigma \colon I \to I$ does not change summability or the sum.

Example: in $\R$, the family $(2^{-n})_{n \ge 0}$ has sum $2$. For $U \supseteq (2 - \varepsilon, 2 + \varepsilon)$ choose $N$ with $2^{-N} < \varepsilon$ and $F_0 = \set{0, \dots, N}$. For finite $F \supseteq F_0$ one has $2 - 2^{-N} \le s_F < 2$, so $s_F \in U$.

Non-example: in $\R$, the family $((-1)^{n+1}/n)_{n \ge 1}$ is not summable. For any finite $F_0$, adding finitely many odd $n$ beyond $F_0$ to $F_0$ makes $s_F$ as large as one likes, because $\sum_{n \text{ odd}} 1/n$ diverges.

In $\R$ and $\C$, a family indexed by $\N$ is summable if and only if it is absolutely convergent, and then the sum equals the sum of the series.