lean_workbook_plus_59127
DisprovedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59127 : ∀ x1 x2 x3 : ℝ, (1 + x1 ^ 3) * (1 + x2 ^ 3) * (1 + x3 ^ 3) ≥ (1 + x1 * x2 * x3) ^ 3 := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_59127 : ∀ x1 x2 x3 : ℝ, (1 + x1 ^ 3) * (1 + x2 ^ 3) * (1 + x3 ^ 3) ≥ (1 + x1 * x2 * x3) ^ 3 := by sorry