En los retículos, x ⊓ y = y ⊓ x
Demostrar con Lean4 que en los retículos se verifica que
\[x ⊓ y = 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 z : α) example : x ⊓ y = y ⊓ x := by sorry |