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