lean_workbook_plus_79397

Open

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

Prove that $f(x)=2^x+\frac{ln(x)}{ln(2)}$ is strictly increasing for $x>0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79397 (x y : ℝ) (hxy : x < y) (hx : 0 < x) (hy : 0 < y) : (2:ℝ)^x + (Real.log x) / (Real.log 2) < (2:ℝ)^y + (Real.log y) / (Real.log 2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph