Prove2Me

lean_workbook_plus_57257

Proved

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

Suppose a,b,ca,b,c are reals then show that ∣a∣+∣b∣+∣c∣+∣a+b+c∣≥∣a+b∣+∣b+c∣+∣c+a∣\left|a\right|+\left|b\right|+\left|c\right|+\left|a+b+c\right|\ge \left|a+b\right|+\left|b+c\right|+\left|c+a\right| .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_57257 (a b c : ℝ) : |a| + |b| + |c| + |a + b + c| ≥ |a + b| + |b + c| + |c + a|   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph