3 enero 2024 – Calculemus

En los órdenes parciales, a < b ↔ a ≤ b ∧ a ≠ b

PorJosé A. Alonso 3 enero 202431 diciembre 2023

Demostrar con Lean4 que en los órdenes parciales,
\[a < b ↔ a ≤ b ∧ a ≠ b\]

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

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]
variable (a b : α)

example : a < b ↔ a ≤ b ∧ a ≠ b :=
by sorry

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]

variable (a b : α)

example : a < b ↔ a ≤ b ∧ a ≠ b :=

by sorry