lean_workbook_plus_48863
ProvedProve that the sequence diverges.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48863 : ¬ ∃ l, ∀ n, |(-1 : ℝ)^n - l| < 1 := by sorry
Source
Prove that the sequence diverges.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_48863 : ¬ ∃ l, ∀ n, |(-1 : ℝ)^n - l| < 1 := by sorry