lean_workbook_plus_27049
ProvedFor , show that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27049 (x : ℝ) (hx : 0 ≤ x ∧ x ≤ 1) : |x * (x - 1) * (x^6 + 2 * x^4 + 3 * x^2 + 4)| < 5 / 2 := by sorry
Source
For , show that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_27049 (x : ℝ) (hx : 0 ≤ x ∧ x ≤ 1) : |x * (x - 1) * (x^6 + 2 * x^4 + 3 * x^2 + 4)| < 5 / 2 := by sorry