lean_workbook_plus_29909

Proved

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

You only need here is $|\,|x|-|y|\,| \le |x-y|,$ which is easily verified by squaring both sides.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29909 (x y : ℝ) : |(abs x) - (abs y)| ≤ abs (x - y)   :=  by sorry

Source