monotone sequence that tends to infinity

Stream: Is there code for X?

[Rémy Degenne]

Do we have something close to this somewhere? (I have a proof, but I think we might already have the lemma or something more general)

lemma exists_seq_monotone_tendsto_at_top_at_top (α : Type*) [semilattice_sup α]
  [(at_top : filter α).ne_bot] [(at_top : filter α).is_countably_generated] :
  ∃ xs : ℕ → α, monotone xs ∧ tendsto xs at_top at_top := sorry

[Rémy Degenne]

Without monotone xs, this is filter.exists_seq_tendsto, but I really want that monotone

[Yaël Dillies]

My instinct would be to apply docs#exists_seq_strict_mono_tendsto to with_top α. Does that work?

[Rémy Degenne]

Yes, it probably works? Up to some back and forth between alpha and the with_top type i guess. As I wrote, I have a proof already (which uses exists_seq_tendsto and then builds a monotone sequence from it). I intentionally did not include it to avoid the inevitable golf contest :) . I just want to check that the lemma is indeed missing from the library.

[Yaël Dillies]

I can attest I do not know of such a lemma.

[Eric Rodriguez]

btw, docs#filter.at_top_ne_bot means you can replace the ne_bot with nonempty \a