Tail of bounded series tends to zero

Stream: Is there code for X?

[Markus Himmel]

Does mathlib have a version of the following?

import measure_theory.measure_space

open filter topological_space
open_locale topological_space

lemma tendsto_sum_add (f : ℕ → ennreal) (hf : (∑' i, f i) < ⊤) :
  tendsto (λ i, ∑' k, f (i + k)) at_top (𝓝 0) := sorry

[Heather Macbeth]

There is docs#summable_iff_vanishing_norm . This covers all f : ι → α with α a normed space and with no structure on ι, so it is more general in two ways, but doesn't cover the ennreal part of what you wrote.