lean_workbook_plus_12563

Proved

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

Now $0 \le (1-x)x=-(x-\frac{1}{2})^2+\frac{1}{4} \le \frac{1}{4}$ for $x \in [0,1]$ , so

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12563  (x : ℝ)
  (h₀ : 0 ≤ x)
  (h₁ : x ≤ 1) :
  0 ≤ (1 - x) * x ∧ (1 - x) * x ≤ 1 / 4   :=  by sorry

Source