real sequences: filter.tends_to vs. classical def.

Stream: Is there code for X?

[Matthias U]

I'm looking for a lemma that says the following (or something similiar): If a:ℕ → ℝ is a real sequence and l:ℝ, then a tends to l, i.e. filter.tendsto a filter.at_top (𝓝 l) if and only if ∀ ε >0, ∃ N, ∀n≥ N, |l - a n| ≤ ε

[Mario Carneiro]

That should be in the file on metric spaces

[Mario Carneiro]

like docs#metric.tendsto_at_top

[Mario Carneiro]

and then docs#real.dist_eq to write it in terms of abs

[Matthias U]

Thank you very much!