En ℝ, |a| – |b| ≤ |a – b|
Demostrar con Lean4 que si \(a\) y \(b\) números reales, entonces
\[|a| – |b| \leq |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 |
Demostraciones en lenguaje natural (LN)
1ª demostración en LN
Por la siguiente cadena de desigualdades
\begin{align}
|a| – |b| &= |a – b + b| – |b| \\
&\leq (|a – b| + |b|) – |b| &&\text{[por la desigualdad triangular]}\\
&= |a – b|
\end{align}
2ª demostración en LN
Por la desigualdad triangular
\[ |a – b + b| \leq |a – b| + |b| \]
simplificando en la izquierda
\[ |a| \leq |a – b| + |b| \]
y, pasando \(|b|\) a la izquierda
\[ |a| – |b| ≤ |a – b| \]
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) -- 1ª demostración (basada en la 1ª en LN) example : |a| - |b| ≤ |a - b| := calc |a| - |b| = |a - b + b| - |b| := congrArg (fun x => |x| - |b|) (sub_add_cancel a b).symm _ ≤ (|a - b| + |b|) - |b| := sub_le_sub_right (abs_add (a - b) b) (|b|) _ = |a - b| := add_sub_cancel (|a - b|) (|b|) -- 2ª demostración (basada en la 1ª en LN) example : |a| - |b| ≤ |a - b| := calc |a| - |b| = |a - b + b| - |b| := by rw [sub_add_cancel] _ ≤ (|a - b| + |b|) - |b| := by apply sub_le_sub_right apply abs_add _ = |a - b| := by rw [add_sub_cancel] -- 3ª demostración (basada en la 2ª en LN) example : |a| - |b| ≤ |a - b| := by have h1 : |a - b + b| ≤ |a - b| + |b| := abs_add (a - b) b rw [sub_add_cancel] at h1 exact abs_sub_abs_le_abs_sub a b -- 4ª demostración example : |a| - |b| ≤ |a - b| := abs_sub_abs_le_abs_sub a b |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 18.
