lean_workbook_plus_60566

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

So there is a $n_0\in\mathbb{N}$ such that for all $n\ge n_0$ then $a_n$ is constant

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60566 (a : ℕ → ℕ) (n₀ : ℕ) (h : ∀ n ≥ n₀, a n = a n₀) : ∃ n₀, ∀ n ≥ n₀, a n = a n₀   :=  by sorry

Source