lean_workbook_plus_39297

Proved

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

Let $\{x_n\}$ be a sequence of real numbers with the property that for any $n\geq 2$ $\exists\ k,$ $\frac{n}{2}<k <n$ , such that $x_n=\frac{x_k }{2}$ , prove that $\lim\limits_{n\to\infty} x_n=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39297 (x : ℕ → ℝ) (hx : ∀ n ≥ 2, ∃ k, n / 2 < k ∧ k < n ∧ x n = x k / 2) : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |x n| < ε   :=  by sorry

Source

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

View graph