lean_workbook_plus_62735
ProvedIf , show that the sequence converges to .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62735 (x : ℕ → ℝ) (x0 : x 0 = Real.sqrt 2) (x_rec : ∀ n, x (n + 1) = (x n + 2 / x n) / 2) : ∃ n, ∀ ε > 0, |x n - Real.sqrt 2| < ε := by sorry
Source