Prove2Me

lean_workbook_plus_18661

Proved

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

prove that ∣a∣+∣b∣+∣c∣+∣a+b+c∣≥∣a+b∣+∣b+c∣+∣a+c∣ \left|a \right|+\left|b \right|+\left|c \right|+\left|a+b+c \right|\geq\left|a+b \right|+\left|b+c \right|+\left|a+c \right|, for all real numbers a,b,ca, b, c

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

View graph