## Stream: Is there code for X?

### Topic: sequence tending to a limit

#### Kevin Buzzard (May 10 2020 at 18:29):

import topology.instances.real

open_locale topological_space

open filter

example (f : ℕ → ℝ) (l : ℝ) :
tendsto f (cofinite) (𝓝 l) ↔ (∀ ε, 0 < ε → ∃ N, ∀ n, N ≤ n → abs (f n - l) < ε) :=
sorry


What is the idiomatic Lean way to say this? Maybe cofinite should be replaced by some "neighbourhood of infinty" filter? Are all these concepts proved to be equivalent somewhere? I'm thinking about the questions Heather Macbeth set her class.

#### Kevin Buzzard (May 10 2020 at 18:34):

I do, but I also think I want the equivalence in my question (with cofinite replaced by at_top if necessary)

#### Kevin Buzzard (May 10 2020 at 18:34):

ooh bingo, library_search

#### Kevin Buzzard (May 10 2020 at 18:36):

Once I changed cofinite to at_top, library_search kicked in. metric.tendsto_at_top

#### Kevin Buzzard (May 10 2020 at 18:38):

Before the change, I can't get any tactic to give me a clue (and I didn't know the name of the at_top filter when I wrote the original post).

#### Mario Carneiro (May 10 2020 at 18:38):

at_top is I think the more canonical way to write this, but cofinite is also a fine filter. I hope the equality is proven somewhere

#### Kevin Buzzard (May 10 2020 at 18:38):

Yes, Reid's first link is the proof

#### Mario Carneiro (May 10 2020 at 18:38):

that should be a simp lemma, I think

Last updated: May 16 2021 at 05:21 UTC