lean_workbook_plus_73036
ProvedUse Cauchy's convergence criterion to show that { } converges where
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_73036 (s : ℕ → ℝ) (hs : ∀ n, s (n + 1) = (s n + s (n - 1)) / 2) : ∀ ε > 0, ∃ N : ℕ, ∀ n > N, |s n - s (n - 1)| < ε := by sorry
Source