Commit 2021-02-04 21:33 d2938225

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.