lean_workbook_plus_39716

Proved

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

Let $x$ , $y$ and $z$ be three real numbers such that : \n\n $\rightarrow \hspace{2mm} |x| \geq |y+z|$ \n\n $\rightarrow \hspace{2mm} |y| \geq |x+z|$ \n\n $\rightarrow \hspace{2mm} |z| \geq |x+y|$ \n\nProve that $x+y+z=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39716 (x y z: ℝ) (hx: abs x ≥ abs (y + z)) (hy: abs y ≥ abs (x + z)) (hz: abs z ≥ abs (x + y)) : x + y + z = 0   :=  by sorry

Source

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

View graph