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