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

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

example
  (h : x ≠ 0)
  : x < 0 ∨ x > 0 :=
by sorry

Demostración en lenguaje natural Usando el siguiente lema \\[ (∀ x y ∈ ℝ)[x < y ∨ x = y ∨ y < x] \\] se demuestra distinguiendo tres casos. Caso 1: Supongamos que \\(x < 0\\). Entonces, se verifica la disyunción ya que se verifica su primera parte. Caso 2: Supongamos que \\(x = 0\\). Entonces, se tiene una contradicción con la hipótesis. Caso 3: Supongamos que \\(x > 0\\). Entonces, se verifica la disyunción ya que se verifica su segunda parte. Demostraciones con Lean4

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

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

example
  (h : x ≠ 0)
  : x < 0 ∨ x > 0 :=
by
  rcases lt_trichotomy x 0 with hx1 | hx2 | hx3
  . -- hx1 : x < 0
    left
    -- ⊢ x < 0
    exact hx1
  . -- hx2 : x = 0
    contradiction
  . -- hx3 : 0 < x
    right
    -- ⊢ x > 0
    exact hx3

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

example
  (h : x ≠ 0)
  : x < 0 ∨ x > 0 :=
Ne.lt_or_lt h

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

example
  (h : x ≠ 0)
  : x < 0 ∨ x > 0 :=
by aesop

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

-- variable (y : ℝ)
-- #check (lt_trichotomy x y : x < y ∨ x = y ∨ y < x)

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

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