lean_workbook_plus_80913

Proved

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

Suppose $a>0,\ |x-1|<\frac {a}{3},\ |y-2|<\frac {a}{3}.$ Prove that $|2x+y-4|<a.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80913 (a : ℝ) (x y : ℝ) (ha : a > 0) (hx : |x - 1| < a / 3) (hy : |y - 2| < a / 3) : |2 * x + y - 4| < a   :=  by sorry

Source