Zulip Chat Archive

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.

Reid Barton (May 10 2020 at 18:31):

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

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

Reid Barton (May 10 2020 at 18:36):

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

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: Dec 20 2023 at 11:08 UTC