Skip to main content

En ℝ, |x + y| ≤ |x| + |y|

Demostrar con Lean4 que en \(ℝ\), \[ |x + y| ≤ |x| + |y| \]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {x y : ℝ}

example : |x + y| ≤ |x| + |y| :=
by sorry

Demostración en lenguaje natural

Se usarán los siguientes lemas \begin{align} &(∀ x ∈ ℝ)[0 ≤ x → |x| = x) \tag{L1} \newline &(∀ a, b, c, d ∈ ℝ)[a ≤ b ∧ c ≤ d → a + c ≤ b + d] \tag{L2} \newline &(∀ x ∈ ℝ)[x ≤ |x|] \tag{L3} \newline &(∀ x ∈ ℝ)[x < 0 → |x| = -x] \tag{L4} \newline &(∀ x, y ∈ ℝ)[-(x + y) = -x + -y] \tag{L5} \newline &(∀ x ∈ ℝ)[-x ≤ |x|] \tag{L6} \end{align}

Se demostrará por casos según \(x + y ≥ 0\):

Primer caso: Supongamos que \(x + y ≥ 0\). Entonces, \begin{align} |x + y| &= x + y &&\text{[por L1]} \newline &≤ |x| + |y| &&\text{[por L2 y L3]} \end{align}

Segundo caso: Supongamos que \(x + y < 0\). Entonces, \begin{align} |x + y| &= -(x + y) &&\text{[por L4]} \newline &= -x + -y &&\text{[por L5]} \newline &≤ |x| + |y| &&\text{[por L2 y L6]} \end{align}

Demostraciones con Lean4

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {x y : ℝ}

-- 1ª demostración
-- ===============

example : |x + y| ≤ |x| + |y| :=
by
  rcases le_or_gt 0 (x + y) with h1 | h2
  · -- h1 : 0 ≤ x + y
    show |x + y| ≤ |x| + |y|
    calc |x + y| = x + y     := by exact abs_of_nonneg h1
               _ ≤ |x| + |y| := add_le_add (le_abs_self x) (le_abs_self y)
  . -- h2 : 0 > x + y
    show |x + y| ≤ |x| + |y|
    calc |x + y| = -(x + y)  := by exact abs_of_neg h2
               _ = -x + -y   := by exact neg_add x y
               _ ≤ |x| + |y| := add_le_add (neg_le_abs x) (neg_le_abs y)

-- 2ª demostración
-- ===============

example : |x + y| ≤ |x| + |y| := by
  rcases le_or_gt 0 (x + y) with h1 | h2
  · -- h1 : 0 ≤ x + y
    rw [abs_of_nonneg h1]
    -- ⊢ x + y ≤ |x| + |y|
    exact add_le_add (le_abs_self x) (le_abs_self y)
  . -- h2 : 0 > x + y
    rw [abs_of_neg h2]
    -- ⊢ -(x + y) ≤ |x| + |y|
    calc -(x + y) = -x + -y    := by exact neg_add x y
                _ ≤ |x| + |y|  := add_le_add (neg_le_abs x) (neg_le_abs y)

-- 2ª demostración
-- ===============

example : |x + y| ≤ |x| + |y| := by
  rcases le_or_gt 0 (x + y) with h1 | h2
  · -- h1 : 0 ≤ x + y
    rw [abs_of_nonneg h1]
    -- ⊢ x + y ≤ |x| + |y|
    linarith [le_abs_self x, le_abs_self y]
  . -- h2 : 0 > x + y
    rw [abs_of_neg h2]
    -- ⊢ -(x + y) ≤ |x| + |y|
    linarith [neg_le_abs x, neg_le_abs y]

-- 3ª demostración
-- ===============

example : |x + y| ≤ |x| + |y| :=
  abs_add x y

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

-- variable (a b c d : ℝ)
-- #check (abs_add x y : |x + y| ≤ |x| + |y|)
-- #check (abs_of_neg : x < 0 → |x| = -x)
-- #check (abs_of_nonneg : 0 ≤ x → |x| = x)
-- #check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
-- #check (le_abs_self a : a ≤ |a|)
-- #check (le_or_gt x y : x ≤ y ∨ x > y)
-- #check (neg_add x y : -(x + y) = -x + -y)
-- #check (neg_le_abs x : -x ≤ |x|)

Demostraciones interactivas

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

Referencias