lean_workbook_plus_50168

Proved

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

Hlawka's inequality follows immediately from the triangle inequality and the following identity (from Hlawka...) : \n\n $(|a|+|b|+|c|-|b+c|-|c+a|-|a+b|+|a+b+c|) \cdot (|a|+|b|+|c|+|a+b+c|) = (|b|+|c|-|b+c|) \cdot (|a|-|b+c| + |a+b+c|) + (|c|+|a|-|c+a|) \cdot (|b|-|c+a|+|a+b+c|) + (|a|+|b| - |a+b|) \cdot (|c|-|a+b|+|a+b+c|).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50168 (a b c : ℝ) : (|a| + |b| + |c| - |b + c| - |c + a| - |a + b| + |a + b + c|) * (|a| + |b| + |c| + |a + b + c|) = (|b| + |c| - |b + c|) * (|a| - |b + c| + |a + b + c|) + (|c| + |a| - |c + a|) * (|b| - |c + a| + |a + b + c|) + (|a| + |b| - |a + b|) * (|c| - |a + b| + |a + b + c|)   :=  by sorry

Source

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

View graph