En los retículos, x ⊔ (x ⊓ y) = x
Demostrar con Lean4 que en los retículos se verifica que
\[ x ⊔ (x ⊓ y) = x \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α]-- variable (x y : α) example : x ⊔ (x ⊓ y) = x := by sorry |