lean_workbook_plus_3143

Proved

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

Triangular inequality $|x - 2y + z| \le |x-y|+|z-y|$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3143 (x y z : ℝ) : |x - 2*y + z| ≤ |x-y| + |z-y|   :=  by sorry

Source