lean_workbook_plus_28973

Proved

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

Prove that if $\lim_{n\to \infty} x_n^{1/n} = d < 1$ , then $\lim_{n\to \infty} x_n = 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28973 (x : ℕ → NNReal) (d : ℝ) (hd : d < 1) (h : ∀ n, (x n)^(1/n) = d) : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x n < ε   :=  by sorry

Source