En los retículos, x ⊔ y = y ⊔ x
Demostrar con Lean4 que en los retículos se verifica que
\[x ⊔ y = y ⊔ x\]
para todo \(x\) e \(y\) en el retículo.
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 |