lean_workbook_plus_15059
ProvedProve that for
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15059 : ∀ P ∈ Set.Icc (3 - 2 * Real.sqrt 2) 4, 2 * P ^ 3 - 10 * P ^ 2 + 9 * P - 4 ≤ 0 := by sorry
Source
Prove that for
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_15059 : ∀ P ∈ Set.Icc (3 - 2 * Real.sqrt 2) 4, 2 * P ^ 3 - 10 * P ^ 2 + 9 * P - 4 ≤ 0 := by sorry