Commit 2021-02-08 14:15 8a23aa3b

feat(topology/instances/{nnreal,ennreal}): add tendsto_cofinite_zero_of_summable (#6093) For f : a -> nnreal, summable f implies tendsto f cofinite (nhds 0). For f : a -> ennreal, tsum f < \top implies tendsto f cofinite (nhds 0). Add versions of these lemmas with at_top instead of cofinite when a = N. Also add ennreal.tendsto_at_top_zero, a simpler statement for a particular case of ennreal.tendsto_at_top.