Si a, b ∈ ℝ, entonces |a| – |b| ≤ |a – b|
Sean a y b números reales. Demostrar que
1 |
|a| - |b| ≤ |a - b| |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 |
import data.real.basic variables a b : ℝ example : |a| - |b| ≤ |a - b| := sorry |
Soluciones con Lean
1 2 3 4 5 6 7 8 9 |
import data.real.basic variables a b : ℝ example : |a| - |b| ≤ |a - b| := calc |a| - |b| = |a - b + b| - |b| : by simp ... ≤ (|a - b| + |b|) - |b| : sub_le_sub_right (abs_add (a - b) b) (|b|) ... = |a - b| : add_sub_cancel (|a - b|) (|b|) |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 20.