lean_workbook_plus_2762
OpenShow that is positive for all positive .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2762 : ∀ x > 0, x - Real.log (1 + x) > 0 := by sorry
Source
Show that is positive for all positive .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_2762 : ∀ x > 0, x - Real.log (1 + x) > 0 := by sorry