English
If u:ℕ→β is unbounded above, then there exists a subsequence φ of ℕ such that φ is strictly increasing and u ∘ φ is strictly increasing.
Русский
Если u не ограничена сверху, существует строгая возрастающая подпоследовательность φ such that u∘φ возрастает строго.
LaTeX
$$$[\text{LinearOrder}(β)] \land [\text{NoMaxOrder}(β)] \;{u: \mathbb{N} \to β} \\ (\operatorname{Tendsto}(u, \operatorname{atTop}, \operatorname{atTop})) \\Rightarrow \exists φ: \mathbb{N} \to \mathbb{N}, \ \operatorname{StrictMono} φ \land \operatorname{StrictMono}(u \circ φ)$$$
Lean4
theorem strictMono_subseq_of_tendsto_atTop [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Tendsto u atTop atTop) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ StrictMono (u ∘ φ) :=
let ⟨φ, h, h'⟩ := extraction_of_frequently_atTop (frequently_high_scores hu)
⟨φ, h, fun _ m hnm => h' m _ (h hnm)⟩
