En los retículos, (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)
Demostrar con Lean4 que en los retículos se verifica que \[(x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y z : α) example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := by sorry
Demostración en lenguaje natural
En la demostración se usarán los siguientes lemas: \begin{align} &x ≤ y → y ≤ x → x = y \tag{L1} \\ &z ≤ x → z ≤ y → z ≤ x ⊓ y \tag{L2} \\ &x ⊓ y ≤ x \tag{L3} \\ &x ⊓ y ≤ y \tag{L4} \end{align}
Por L1, es suficiente demostrar las siguientes relaciones: \begin{align} (x ⊓ y) ⊓ z &≤ x ⊓ (y ⊓ z) \tag{1} \\ x ⊓ (y ⊓ z) &≤ (x ⊓ y) ⊓ z \tag{2} \end{align}
Para demostrar (1), por L2, basta probar que \begin{align} (x ⊓ y) ⊓ z ≤ x \tag{1a} \\ (x ⊓ y) ⊓ z ≤ y ⊓ z \tag{1b} \end{align}
La (1a) se demuestra por la siguiente cadena de desigualdades \begin{align} (x ⊓ y) ⊓ z &≤ x ⊓ y &&\text{[por L3]} \\ &≤ x &&\text{[por L3]} \end{align}
Para demostrar (1b), por L2, basta probar que \begin{align} (x ⊓ y) ⊓ z &≤ y \tag{1b1} \\ (x ⊓ y) ⊓ z &≤ z \tag{1b2} \end{align}
La (1b1) se demuestra por la siguiente cadena de desigualdades \begin{align} (x ⊓ y) ⊓ z &≤ x ⊓ y &&\text{[por L3]} \\ &≤ y &&\text{[por L4]} \end{align}
La (1b2) se tiene por L4.
Para demostrar (2), por L2, basta probar que \begin{align} x ⊓ (y ⊓ z) &≤ x ⊓ y \tag{2a} \\ x ⊓ (y ⊓ z) &≤ z \tag{2b} \end{align}
Para demostrar (2a), por L2, basta probar que \begin{align} x ⊓ (y ⊓ z) &≤ x \tag{2a1} \\ x ⊓ (y ⊓ z) &≤ y \tag{2a2} \end{align}
La (2a1) se tiene por L3.
La (2a2) se demuestra por la siguiente cadena de desigualdades \begin{align} x ⊓ (y ⊓ z) &≤ y ⊓ z &&\text{[por L4]} \\ &≤ y &&\text{[por L3]} \end{align}
La (2b) se demuestra por la siguiente cadena de desigualdades \begin{align} x ⊓ (y ⊓ z) &≤ y ⊓ z &&\text{[por L4]} \\ &≤ z &&\text{[por L4]} \end{align}
Demostraciones con Lean4
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y z : α) -- 1ª demostración -- =============== example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := by have h1 : (x ⊓ y) ⊓ z ≤ x ⊓ (y ⊓ z) := by { have h1a : (x ⊓ y) ⊓ z ≤ x := calc (x ⊓ y) ⊓ z ≤ x ⊓ y := by exact inf_le_left _ ≤ x := by exact inf_le_left have h1b : (x ⊓ y) ⊓ z ≤ y ⊓ z := by { have h1b1 : (x ⊓ y) ⊓ z ≤ y := calc (x ⊓ y) ⊓ z ≤ x ⊓ y := by exact inf_le_left _ ≤ y := by exact inf_le_right have h1b2 : (x ⊓ y) ⊓ z ≤ z := inf_le_right show (x ⊓ y) ⊓ z ≤ y ⊓ z exact le_inf h1b1 h1b2 } show (x ⊓ y) ⊓ z ≤ x ⊓ (y ⊓ z) exact le_inf h1a h1b } have h2 : x ⊓ (y ⊓ z) ≤ (x ⊓ y) ⊓ z := by { have h2a : x ⊓ (y ⊓ z) ≤ x ⊓ y := by { have h2a1 : x ⊓ (y ⊓ z) ≤ x := inf_le_left have h2a2 : x ⊓ (y ⊓ z) ≤ y := calc x ⊓ (y ⊓ z) ≤ y ⊓ z := by exact inf_le_right _ ≤ y := by exact inf_le_left show x ⊓ (y ⊓ z) ≤ x ⊓ y exact le_inf h2a1 h2a2 } have h2b : x ⊓ (y ⊓ z) ≤ z := by calc x ⊓ (y ⊓ z) ≤ y ⊓ z := by exact inf_le_right _ ≤ z := by exact inf_le_right show x ⊓ (y ⊓ z) ≤ (x ⊓ y) ⊓ z exact le_inf h2a h2b } show (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) exact le_antisymm h1 h2 -- 2ª demostración -- =============== example : x ⊓ y ⊓ z = x ⊓ (y ⊓ z) := by apply le_antisymm · apply le_inf · apply le_trans apply inf_le_left apply inf_le_left . apply le_inf · apply le_trans apply inf_le_left apply inf_le_right . apply inf_le_right . apply le_inf · apply le_inf · apply inf_le_left . apply le_trans apply inf_le_right apply inf_le_left . apply le_trans apply inf_le_right apply inf_le_right -- 3ª demostración -- =============== example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := by apply le_antisymm . apply le_inf . apply inf_le_of_left_le inf_le_left . apply le_inf (inf_le_of_left_le inf_le_right) inf_le_right . apply le_inf . apply le_inf inf_le_left (inf_le_of_right_le inf_le_left) . apply inf_le_of_right_le inf_le_right -- 4ª demostración -- =============== example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := le_antisymm (le_inf (inf_le_of_left_le inf_le_left) (le_inf (inf_le_of_left_le inf_le_right) inf_le_right)) (le_inf (le_inf inf_le_left (inf_le_of_right_le inf_le_left)) (inf_le_of_right_le inf_le_right)) -- 5ª demostración -- =============== example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := -- by apply? inf_assoc x y z -- Lemas usados -- ============ -- #check (inf_assoc x y z : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)) -- #check (inf_le_left : x ⊓ y ≤ x) -- #check (inf_le_of_left_le : x ≤ z → x ⊓ y ≤ z) -- #check (inf_le_of_right_le : y ≤ z → x ⊓ y ≤ z) -- #check (inf_le_right : x ⊓ y ≤ y) -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) -- #check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y) -- #check (le_trans : x ≤ y → y ≤ z → x ≤ z)
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 21.