lean_workbook_plus_56484

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Lemma: For every integer number $k \ge 1$ we have that $2^{k-1} \ge k$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_56484 (k : ℕ) : 2 ^ (k - 1) ≥ k   :=  by sorry

Source