Countability from vanishing averages of distinct sequences (source code)

= Countability from vanishing averages of distinct sequences

If every <sequence> of distinct elements of a positive-real <set> $A$ has arithmetic averages tending to zero, then $A$ is a <countable set>. For each positive <integer> $n$, the threshold <set> $\{a\in A:a\ge1/n\}$ must be finite: an infinite sequence inside it would have averages at least $1/n$. The <Archimedean property> makes $A$ their union, so the <countable union of countable sets> theorem applies. The hypothesis concerns every distinct-element sequence, not merely one enumeration.