lean_workbook_plus_2613

Proved

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

$\textbf{Case 1: }$ For $x_1=x_0: x_n=x_0,\;\forall n\in\mathbb{N}$ . In this case, the sequence $(x_n)_{n\in\mathbb{N}}$ is constant, hence convergent.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2613 (x : ℕ → ℝ) (x0 : ℝ) (h : ∀ n, x n = x0) : ∃ l, ∀ ε > 0, ∃ N, ∀ n ≥ N, |x n - l| < ε   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph