En ℝ, |a| – |b| ≤ |a – b|
Demostrar con Lean4 que si a y b números reales, entonces
|a|–|b|≤|a–b|
Para ello, completar la siguiente teoría de Lean4:
Demostrar con Lean4 que si a y b números reales, entonces
|a|–|b|≤|a–b|
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : |a| - |b| ≤ |a - b| := by sorry |