En ℝ, |x + y| ≤ |x| + |y|
Demostrar con Lean4 que en \(ℝ\),
\[ |x + y| ≤ |x| + |y| \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example : |x + y| ≤ |x| + |y| := by sorry |