lean_workbook_plus_2315

Proved

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

Take a Cauchy sequence $\{x_n\}$ and construct a subsequence $\{x_{n_k}\}$ such that $\lVert x_{n_{k+1}}-x_{n_k}\rVert\leq 2^{-k}$ for all $k$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2315 (x : ℕ → ℝ) (hx : CauchySeq x) :
    ∃ n : ℕ → ℕ, ∀ k : ℕ, ‖x (n (k + 1)) - x (n k)‖ ≤ (1 / 2)^k   :=  by sorry

Source