lean_workbook_plus_7664

Proved

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

Prove that for real numbers $a, b, c$ ,\n\n

|a+b| + |b+c| + |c+a| \le |a|+|b|+|c| + |a+b+c|.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7664 (a b c : ℝ) : |a + b| + |b + c| + |c + a| ≤ |a| + |b| + |c| + |a + b + c|   :=  by sorry

Source