## 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: May 11 2021 at 22:14 UTC