lean_workbook_plus_39376

Disproved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

if $-1\leq x \leq0$ then $g(x)=-2x^2-2x+2=-2(x+1/2)^2+\frac{5}4\leq\frac{5}4$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39376 (x : ℝ) (hx : -1 ≤ x ∧ x ≤ 0) :
  -2 * x ^ 2 - 2 * x + 2 ≤ 5 / 4   :=  by sorry

Source