sequence tending to a limit

Stream: Is there code for X?

[Kevin Buzzard]

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.

[Reid Barton]

You want this: https://leanprover-community.github.io/mathlib_docs/order/filter/basic.html#filter.nat.cofinite_eq_at_top

[Kevin Buzzard]

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

[Kevin Buzzard]

ooh bingo, library_search

[Reid Barton]

related: https://www.codewars.com/kata/reviews/5ea1f38e014f0c0001ec7c70/groups/5ea612e99de75200013c0854

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

Yes, Reid's first link is the proof

[Mario Carneiro]

that should be a simp lemma, I think