Skip to main content

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:

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

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_right (|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_right]

-- 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

-- Lemas usados
-- ============

-- #check (abs_add a b : |a + b| ≤ |a| + |b|)
-- #check (abs_sub_abs_le_abs_sub a b : |a| - |b| ≤ |a - b|)
-- #check (add_sub_cancel_right a b : a + b - b = a)
-- #check (sub_add_cancel a b : a - b + b = a)
-- #check (sub_le_sub_right : a ≤ b → ∀ (c : ℝ), a - c ≤ b - c)

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias