lean_workbook_plus_78652
ProvedProve that the sequence is bounded
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78652 : ∃ M, ∀ n, |(1:ℝ) / 2 ^ n| ≤ M := by sorry
Source
Prove that the sequence is bounded
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_78652 : ∃ M, ∀ n, |(1:ℝ) / 2 ^ n| ≤ M := by sorry