--- Título: En ℝ, si x < |y|, entonces x < y ó x < -y. Autor: José A. Alonso --- [mathjax] Demostrar con Lean4 que en \\(ℝ\\), si \\(x < |y|\\), entonces \\(x < y\\) ó \\(x < -y\\). Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic
variable {x y : ℝ}

example : x < |y| → x < y ∨ x < -y :=
by sorry

Demostración en lenguaje natural Se demostrará por casos según \\(y ≥ 0\\). Primer caso: Supongamos que \\(y ≥ 0\\). Entonces, \\(|y| = y\\) y, por tanto, \\(x < y\\). Segundo caso: Supongamos que \\(y < 0\\). Entonces, \\(|y| = -y\\) y, por tanto, \\(x < -y\\). Demostraciones con Lean4

import Mathlib.Data.Real.Basic
variable {x y : ℝ}

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

example : x < |y| → x < y ∨ x < -y :=
by
  intro h1
  -- h1 : x < |y|
  -- ⊢ x < y ∨ x < -y
  cases' le_or_gt 0 y with h2 h3
  . -- h2 : 0 ≤ y
    left
    -- ⊢ x < y
    rwa [abs_of_nonneg h2] at h1
  . -- h3 : 0 > y
    right
    -- ⊢ x < -y
    rwa [abs_of_neg h3] at h1

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

example : x < |y| → x < y ∨ x < -y :=
lt_abs.mp

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

-- #check (le_or_gt x y : x ≤ y ∨ x > y)
-- #check (abs_of_nonneg : 0 ≤ x → abs x = x)
-- #check (abs_of_neg : x < 0 → abs x = -x)
-- #check (lt_abs : x < |y| ↔ x < y ∨ x < -y)

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

J. Avigad y P. Massot. Mathematics in Lean, p. 38.