abs_sub.md

Título	Autor
En ℝ, |a| - |b| ≤ |a - b|	José A. Alonso

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:

import Mathlib.Data.Real.Basic

variable (a b : ℝ)

example : |a| - |b| ≤ |a - b| :=
by sorry

Demostraciones en lenguaje natural (LN)

[mathjax] 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

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.