lean_workbook_plus_70549
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70549 (a_0 a_n : ℝ) (n : ℕ) : a_n ≥ a_0 / (2^n) ↔ (2^n) * a_n ≥ a_0 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_70549 (a_0 a_n : ℝ) (n : ℕ) : a_n ≥ a_0 / (2^n) ↔ (2^n) * a_n ≥ a_0 := by sorry