Zulip Chat Archive

Stream: Is there code for X?

Topic: sequence tending to a limit


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (May 10 2020 at 18:34):

ooh bingo, library_search

view this post on Zulip Reid Barton (May 10 2020 at 18:36):

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

view this post on Zulip Kevin Buzzard (May 10 2020 at 18:36):

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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 10 2020 at 18:38):

Yes, Reid's first link is the proof

view this post on Zulip 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