lean_workbook_plus_47302
ProvedProve the triangle inequality: .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_47302 (a b : ℝ) : |a| - |b| ≤ |a + b| ∧ |a + b| ≤ |a| + |b| := by sorry
Source
Prove the triangle inequality: .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_47302 (a b : ℝ) : |a| - |b| ≤ |a + b| ∧ |a + b| ≤ |a| + |b| := by sorry