--- Título: Si ≤ es un preorden, entonces < es irreflexiva Autor: José A. Alonso --- [mathjax] Demostrar con Lean4 que si \\(≤\\) es un preorden, entonces \\(<\\) es irreflexiva. Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable {α : Type _} [Preorder α]
variable (a : α)

example : ¬a < a :=
by sorry

Demostración en lenguaje natural Se usará la siguiente propiedad de lo preórdenes \\[ (∀ a, b)[a < b ↔ a ≤ b ∧ b ≰ a] \\] Con dicha propiedad, lo que tenemos que demostrar se transforma en \\[ ¬(a ≤ a ∧ a ≰ a) \\] Para demostrarla, supongamos que \\[ a ≤ a ∧ a ≰ a \\] lo que es una contradicción. Demostraciones con Lean4

import Mathlib.Tactic
variable {α : Type _} [Preorder α]
variable (a : α)

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

example : ¬a < a :=
by
  rw [lt_iff_le_not_le]
  -- ⊢ ¬(a ≤ a ∧ ¬a ≤ a)
  rintro ⟨h1, h2⟩
  -- h1 : a ≤ a
  -- h2 : ¬a ≤ a
  -- ⊢ False
  exact h2 h1

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

example : ¬a < a :=
  irrefl a

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

-- variable (b : α)
-- #check (lt_iff_le_not_le : a < b ↔ a ≤ b ∧ ¬b ≤ a)
-- #check (irrefl a : ¬a < a)

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

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