lean_workbook_plus_40882

Proved

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

Minimize $Z=X+3Y$ \n\nsubject to\n\n $2x + y≤10$ \n\n $5X + 2y ≥ 20$ \n\n $-X + 2y ≥ 0$ \n\n $x≥0, y≥0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40882 (x y : ℝ) : (2*x + y ≤ 10 ∧ 5*x + 2*y ≥ 20 ∧ -x + 2*y ≥ 0 ∧ x >= 0 ∧ y >= 0) → x + 3*y >= 7   :=  by sorry

Source