mathlib3

8a23aa3b - feat(topology/instances/{nnreal,ennreal}): add tendsto_cofinite_zero_of_summable (#6093)

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`.