at_top filter for sequences

Stream: new members

[Dan Stanescu]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

docs#filter.unbounded_of_tendsto_at_top probably helps

[Patrick Massot]

and lemmas around that

[Dan Stanescu]

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]

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,