mathlib3

d2938225 - feat(topology/algebra/infinite_sum, topology/instances/ennreal): extend tsum API (#6017)

feat(topology/algebra/infinite_sum, topology/instances/ennreal): extend tsum API (#6017) Lemma `tsum_lt_of_nonneg` shows that if a sequence `f` with non-negative terms is dominated by a sequence `g` with summable series and at least one term of `f` is strictly smaller than the corresponding term in `g`, then the series of `f` is strictly smaller than the series of `g`. Besides this lemma, I also added the relevant API in topology.algebra.infinite_sum.