lean_workbook_plus_51478

Proved

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

Prove that for $k, l, m \in \mathbb{N}$ , $2^{k+l} + 2^{l+m} + 2^{m+k} \leq 2^{k+l+m+1} + 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_51478 (k l m : ℕ) : 2 ^ (k + l) + 2 ^ (l + m) + 2 ^ (m + k) ≤ 2 ^ (k + l + m + 1) + 1   :=  by sorry

Source