English
There exists a sequence xs:ℕ→α which is monotone and tends to atTop along atTop.
Русский
Существует монотонная последовательность xs:ℕ→α, стремящаяся к atTop вдоль atTop.
LaTeX
$$$$\exists xs:\mathbb{N}\to \alpha\;\big(\operatorname{Monotone}(xs) \land \operatorname{Tendsto}(xs, \text{atTop}, \text{atTop})\big).$$$$
Lean4
theorem exists_seq_monotone_tendsto_atTop_atTop (α : Type*) [Preorder α] [Nonempty α] [IsDirected α (· ≤ ·)]
[(atTop : Filter α).IsCountablyGenerated] : ∃ xs : ℕ → α, Monotone xs ∧ Tendsto xs atTop atTop :=
by
obtain ⟨ys, h⟩ := exists_seq_tendsto (atTop : Filter α)
choose c hleft hright using exists_ge_ge (α := α)
set xs : ℕ → α := fun n => (List.range n).foldl (fun x n ↦ c x (ys n)) (ys 0)
have hsucc (n : ℕ) : xs (n + 1) = c (xs n) (ys n) := by simp [xs, List.range_succ]
refine ⟨xs, ?_, ?_⟩
· refine monotone_nat_of_le_succ fun n ↦ ?_
rw [hsucc]
apply hleft
· refine (tendsto_add_atTop_iff_nat 1).1 <| tendsto_atTop_mono (fun n ↦ ?_) h
rw [hsucc]
apply hright
