lean_workbook_plus_54547
ProvedCreate a sequence satisfying:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_54547 : ∃ a : ℕ → ℤ, a 0 = 2 ∧ ∀ n, a (n + 1) = 2 * a n - 1 := by sorry
Source
Create a sequence satisfying:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_54547 : ∃ a : ℕ → ℤ, a 0 = 2 ∧ ∀ n, a (n + 1) = 2 * a n - 1 := by sorry