Si ≤ es un preorden, entonces < es transitiva
Demostrar con Lean4 que si \(≤\) es un preorden, entonces \(<\) es transitiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic variable {α : Type _} [Preorder α] variable (a b c : α) example : a < b → b < c → a < c := by sorry |