lean_workbook_plus_10555
ProvedProve that for all
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10555 (a b : ℝ) : |(abs a) - (abs b)| ≤ abs (a - b) := by sorry
Source
Prove that for all
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_10555 (a b : ℝ) : |(abs a) - (abs b)| ≤ abs (a - b) := by sorry