Zulip Chat Archive

Stream: new members

Topic: at_top filter for sequences

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.

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

Kevin Buzzard (Jul 24 2020 at 16:57):

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

Patrick Massot (Jul 24 2020 at 17:10):

docs#filter.unbounded_of_tendsto_at_top probably helps

Patrick Massot (Jul 24 2020 at 17:11):

and lemmas around that

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

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