lean_workbook_plus_50350
OpenShow that for ,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_50350 (x : ℝ) (hx : 1 < x) : Real.log (x * (x ^ 2 + 3) / (3 * x ^ 2 + 1)) < x := by sorry
Source
Show that for ,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_50350 (x : ℝ) (hx : 1 < x) : Real.log (x * (x ^ 2 + 3) / (3 * x ^ 2 + 1)) < x := by sorry