lean_workbook_plus_34982

Proved

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

Use part (i) to find the greatest value of $xy^{2}$ in the region of the $x-y$ plane given by $x \geq0, y \geq 0$ and $x+2y \leq 3$ . For what values of $x$ and $y$ is this greatest value achieved?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34982 (x y : ℝ) (hx: x ≥ 0 ∧ y ≥ 0 ∧ x + 2*y ≤ 3): x*y^2 ≤ 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph