Infinite sum on a topological monoid The at_top filter on finset α is the limit of all finite sets towards the entire type. So we sum up bigger and bigger sets. This sum operation is still invariant under reordering, and a absolute sum operator.

This is based on Mario Carneiro's infinite sum in Metamath.

For the definition or many statements, α does not need to be a topological monoid. We only add this assumption later, for the lemmas where it is relevant.

summable f means that f has some (infinite) sum. Use tsum to get the value.

tsum f is the sum of f it exists, or 0 otherwise