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 |