English
If a sequence u:ℕ→β is unbounded above and u converges to atTop, then for every N there exists n≥N such that u(n) is strictly greater than all previous terms.
Русский
Если последовательность u:ℕ→β неограничена сверху и u стремится к бесконечности, то после любого N существует n≥N, для которого u(n) больше всех предыдущих членов.
LaTeX
$$$\text{LinearOrder}(\β) \land \text{NoMaxOrder}(\β) \land u: \mathbb{N} \to \β \\ (\operatorname{Tendsto}(u, \operatorname{atTop}, \operatorname{atTop})) \\Rightarrow \forall N, \exists n \ge N, \forall k < n, u(k) < u(n)$$$
Lean4
/-- If `u` is a sequence which is unbounded above,
then after any point, it reaches a value strictly greater than all previous values.
-/
theorem high_scores [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Tendsto u atTop atTop) :
∀ N, ∃ n ≥ N, ∀ k < n, u k < u n := by
intro N
obtain ⟨k : ℕ, - : k ≤ N, hku : ∀ l ≤ N, u l ≤ u k⟩ : ∃ k ≤ N, ∀ l ≤ N, u l ≤ u k :=
exists_max_image _ u (finite_le_nat N) ⟨N, le_refl N⟩
have ex : ∃ n ≥ N, u k < u n := exists_lt_of_tendsto_atTop hu _ _
obtain ⟨n : ℕ, hnN : n ≥ N, hnk : u k < u n, hn_min : ∀ m, m < n → N ≤ m → u m ≤ u k⟩ :
∃ n ≥ N, u k < u n ∧ ∀ m, m < n → N ≤ m → u m ≤ u k :=
by
rcases Nat.findX ex with ⟨n, ⟨hnN, hnk⟩, hn_min⟩
push_neg at hn_min
exact ⟨n, hnN, hnk, hn_min⟩
use n, hnN
rintro (l : ℕ) (hl : l < n)
have hlk : u l ≤ u k := by
rcases (le_total l N : l ≤ N ∨ N ≤ l) with H | H
· exact hku l H
· exact hn_min l hl H
calc
u l ≤ u k := hlk
_ < u n := hnk
