lean_workbook_plus_17430
ProvedShow that the series converges
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_17430 : ∃ y, (∑' k : ℕ, (1:ℝ) / 2 ^ k) = y := by sorry
Source
Show that the series converges
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_17430 : ∃ y, (∑' k : ℕ, (1:ℝ) / 2 ^ k) = y := by sorry