Limit of addition of functions

Stream: Is there code for X?

[Ashvni Narayanan]

I am looking for a lemma of the form :

example {X : Type*} [topological_space X] [t2_space X] [add_comm_monoid X] [has_continuous_add X]
  (f g : ℕ → X) : lim filter.at_top (λ x : ℕ, f x + g x) = lim filter.at_top (λ x : ℕ, f x) + lim filter.at_top (λ x : ℕ, g x) := sorry

Any help is appreciated. Thank you!

[Sebastien Gouezel]

Have a look at docs#filter.tendsto.add

[Sebastien Gouezel]

The lemma as you wrote it can not be true (what happens if one function is not converging?). In general, don't use lim, and use tendsto instead.

[Ashvni Narayanan]

Sebastien Gouezel said:

The lemma as you wrote it can not be true (what happens if one function is not converging?). In general, don't use lim, and use tendsto instead.

Thank you! I know this is not true in general, I was looking for a better lemma that has probably already formulated it.