Prove2Me

Lean-Workbook Plus 52857: Strict monotonicity of real exponential powers

Proved
WorkbookRestored.plus_52857

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

If b>1b>1, then bx<byb^x<b^y for all real x<yx<y.

Source: Lean-Workbook row lean_workbook_plus_52857 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.SpecialFunctions.Pow.Real
Formal statement
theorem WorkbookRestored.plus_52857 (b : ℝ) (hb : 1 < b) : ∀ x y : ℝ, x < y → b^x < b^y   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_52857; immutable original Prove2Me node abddddea-df9c-48e6-947b-d09c8600a63d

View graph