lean_workbook_plus_74648
Provedprove that :
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_74648 (w : ℝ) : 2 * w ^ 2 + 9 ≥ 6 * Real.sqrt 2 * w := by sorry
Source
prove that :
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_74648 (w : ℝ) : 2 * w ^ 2 + 9 ≥ 6 * Real.sqrt 2 * w := by sorry