Zulip Chat Archive

Stream: new members

Topic: at_top filter for sequences


view this post on Zulip Dan Stanescu (Jul 24 2020 at 15:58):

Looking for the best/easiest way to get this:

import data.real.basic
import topology.sequences

open filter

example (s :   ) (L : ) (h :  n : , s n < L) : ¬ (tendsto s at_top at_top) := sorry

In my particular application I can probably get around it, but solving this goal would be much better.

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 16:56):

You could presumably just prove it by unfolding the definition and then inserting the neighborhood (L,infty) directly into the definition

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 16:57):

But there might be a general lemma about bounded implies not tendsto top

view this post on Zulip Patrick Massot (Jul 24 2020 at 17:10):

docs#filter.unbounded_of_tendsto_at_top probably helps

view this post on Zulip Patrick Massot (Jul 24 2020 at 17:11):

and lemmas around that

view this post on Zulip Dan Stanescu (Jul 24 2020 at 17:14):

Patrick Massot said:

docs#filter.unbounded_of_tendsto_at_top probably helps

This does, indeed! Somehow I missed it, although I was "sure" there needed to be something like that. I could use tendsto_at_top_csupr for the positive result, but this helps a lot. Thank you both! @Patrick Massot @Kevin Buzzard

view this post on Zulip Yury G. Kudryashov (Jul 24 2020 at 20:38):

Another option (writing without testing):

intro h : tendsto s at_top at_top,
have :  n, L  s n := (h.eventually (eventually_ge_at_top L)).exists,

Last updated: May 11 2021 at 22:14 UTC