Skip to main content

Si ≤ es un preorden, entonces < es irreflexiva

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