lean_workbook_plus_10959

Proved

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

Let $a,b,c$ be real numbers such that $a+b+c=0$ and $|a|+|b|+|c|=1$ . Prove that

a+\frac{b}{2}+\frac{c}{3}\leq\frac{1}{3}.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10959 (a b c : ℝ) (h1 : a + b + c = 0) (h2 : abs a + abs b + abs c = 1) :
  a + b / 2 + c / 3 ≤ 1 / 3   :=  by sorry

Source