Lean-Workbook Plus 76059: The range of a real exponential with base above one

Proved

WorkbookRestored.plus_76059

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

lean-workbookrestored-importssource-checked

For real $b>1$ , the range of $x\mapsto b^x$ is exactly $(0,\infty)$ .

Source: Lean-Workbook row lean_workbook_plus_76059 (Apache-2.0), original record. This repair only restores required imports and namespaces; the mathematical declaration is unchanged.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Base

Formal statement

theorem WorkbookRestored.plus_76059 (b : ℝ) (hb : 1 < b) : Set.range (λ x : ℝ => b^x) = Set.Ioi 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_76059; immutable original Prove2Me node c4969034-6e6e-4849-b054-5dde6cc9c1e1

View graph