lean_workbook_plus_65524

Proved

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

For $x,y \in R$ such that $\frac{x^2}{2} \le y \le -2x^2 + 3x$ , prove that $x^2 + y^2 \le 2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65524 (x y : ℝ) (h₁ : x ^ 2 / 2 ≤ y) (h₂ : y ≤ -2 * x ^ 2 + 3 * x) : x ^ 2 + y ^ 2 ≤ 2   :=  by sorry

Source