Demostrar con Lean4 que si \(≤\) es un preorden, entonces \(<\) es transitiva.

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

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

example : a < b → b < c → a < c :=
by sorry

Leer más…

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

Leer más…