lean_workbook_plus_17667
OpenProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_17667 : ∀ x y : ℝ, x > 0 ∧ y > 0 → x^4*y^4 ≥ x^3*y^3 + Real.log (x*y) := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_17667 : ∀ x y : ℝ, x > 0 ∧ y > 0 → x^4*y^4 ≥ x^3*y^3 + Real.log (x*y) := by sorry