English
A monotone function f: ℕ → ℕ that is bounded converges: there exist b and N such that for all n ≥ N, f(n) = b.
Русский
Монотонная функция f: ℕ → ℕ, ограниченная сверху, сходится: существует b и N such that для всех n ≥ N, f(n) = b.
LaTeX
$$$\\forall f:\\mathbb{N}\\to\\mathbb{N},\\ Monotone f\\to \\forall c:\\mathbb{N},\\ (\\forall n, f(n) \\le c)\\to \\exists b\\,\\exists N,\\forall n≥N,\\ f(n)=b.$$$
Lean4
/-- A bounded monotone function `ℕ → ℕ` converges. -/
theorem converges_of_monotone_of_bounded {f : ℕ → ℕ} (mono_f : Monotone f) {c : ℕ} (hc : ∀ n, f n ≤ c) :
∃ b N, ∀ n ≥ N, f n = b := by
induction c with
| zero => use 0, 0, fun n _ ↦ Nat.eq_zero_of_le_zero (hc n)
| succ c ih =>
by_cases h : ∀ n, f n ≤ c
· exact ih h
· push_neg at h; obtain ⟨N, hN⟩ := h
replace hN : f N = c + 1 := by specialize hc N; omega
use c + 1, N; intro n hn
specialize mono_f hn; specialize hc n; cutsat
