Prove2Me

lean_workbook_plus_24143

Proved

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

Prove that ∣a+b−c∣+∣b+c−a∣+∣c+a−b∣≥∣a−b∣+∣b−c∣+∣c−a∣ \lvert{a + b - c}\rvert + \lvert{b + c - a}\rvert + \lvert {c + a - b}\rvert \ge \lvert {a - b}\rvert + \lvert{b - c}\rvert + \lvert{c - a}\rvert

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

View graph