lean_workbook_plus_43357
ProvedFind the limit of as approaches infinity for the sequence defined by:\nx_1=\frac{1}{2}\nx_{n+1}=\frac{nx_n^2}{1+(n+1)x_n}$
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_43357 (x : ℕ → ℝ) (hx : x 1 = 1 / 2 ∧ ∀ n, x (n + 1) = n * x n ^ 2 / (1 + (n + 1) * x n)) : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |n * x n| < ε := by sorry
Source