lean_workbook_plus_18195

Proved

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

With the inequality $\frac{x(3-x)}{7-x} \le \frac{2}{9}x+\frac{1}{9}$ being true for $x\in [0,3]$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18195 (x : ℝ) (hx: 0 ≤ x ∧ x ≤ 3) :
  x * (3 - x) / (7 - x) ≤ 2 / 9 * x + 1 / 9   :=  by sorry

Source