English
If a sequence u is unbounded above, then there are infinitely many indices n such that u(k) < u(n) for all k < n.
Русский
Если последовательность неограничена сверху, то существует бесконечно много индексов n, для которых u(k) < u(n) для всех k<n.
LaTeX
$$$\text{LinearOrder}(\β) \land \text{NoMaxOrder}(\β) \land u: \mathbb{N} \to \β \\ (\operatorname{Tendsto}(u, \operatorname{atTop}, \operatorname{atTop})) \\Rightarrow \exists^\infty n \in \operatorname{atTop}, \ \forall k < n, u(k) < u(n)$$$
Lean4
/-- If `u` is a sequence which is unbounded above,
then it `Frequently` reaches a value strictly greater than all previous values.
-/
theorem frequently_high_scores [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Tendsto u atTop atTop) :
∃ᶠ n in atTop, ∀ k < n, u k < u n := by simpa [frequently_atTop] using high_scores hu
