English
If a sequence u:ℕ→β is unbounded below, then after any point it reaches a value strictly smaller than all previous values.
Русский
Если последовательность u:ℕ→β не ограничена снизу, после любой точки она достигает значения, меньше любого предыдущего.
LaTeX
$$$\text{LinearOrder}(\β) \land \text{NoMinOrder}(\β) \land u: \mathbb{N} \to \β \\ (\operatorname{Tendsto}(u, \operatorname{atTop}, \operatorname{atBot})) \\Rightarrow \forall N, \exists n \ge N, \forall k < n, u(n) < u(k)$$$
Lean4
/-- If `u` is a sequence which is unbounded below,
then after any point, it reaches a value strictly smaller than all previous values.
-/
theorem low_scores [LinearOrder β] [NoMinOrder β] {u : ℕ → β} (hu : Tendsto u atTop atBot) :
∀ N, ∃ n ≥ N, ∀ k < n, u n < u k :=
@high_scores βᵒᵈ _ _ _ hu
