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:
|
1 2 3 4 5 6 7 |
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} \label{L1} \\
&x ≤ x ⊔ y \tag{L2} \label{L2} \\
&y ≤ x ⊔ y \tag{L3} \label{L3} \\
&x ≤ z → y ≤ z → x ⊔ y ≤ z \tag{L4} \label{L4} \\
\end{align}
Por \ref{L1}, basta demostrar las siguientes relaciones:
\begin{align}
(x ⊔ y) ⊔ z &≤ x ⊔ (y ⊔ z) \tag{1} \label{1} \\
x ⊔ (y ⊔ z) &≤ (x ⊔ y) ⊔ z \tag{2} \label{2}
\end{align}
Para demostrar (\ref{1}), por \ref{L4}, basta probar
\begin{align}
x ⊔ y &≤ x ⊔ (y ⊔ z) \tag{1a} \label{1a} \\
z &≤ x ⊔ (y ⊔ z) \tag{1b} \label{1b}
\end{align}
Para demostrar (\ref{1a}), por \ref{L4}, basta probar
\begin{align}
x &≤ x ⊔ (y ⊔ z) \tag{1a1} \label{1a1} \\
y &≤ x ⊔ (y ⊔ z) \tag{1a2} \label{1a2}
\end{align}
La (\ref{1a1}) se tiene por \ref{L2}.
La (\ref{1a2}) se tiene por la siguiente cadena de desigualdades:
\begin{align}
y &≤ y ⊔ z &&\text{[por \ref{L2}]} \\
&≤ x ⊔ (y ⊔ z) &&\text{[por \ref{L3}]}
\end{align}
La (\ref{1b}) se tiene por la siguiente cadena de desigualdades
\begin{align}
z &≤ y ⊔ z &&\text{[por \ref{L3}]} \\
&≤ x ⊔ (y ⊔ z) &&\text{[por \ref{L3}]}
\end{align}
Para demostrar (\ref{2}), por \ref{L4}, basta probar
\begin{align}
x &≤ (x ⊔ y) ⊔ z \tag{2a} \label{2a} \\
y ⊔ z &≤ (x ⊔ y) ⊔ z \tag{2b} \label{2b}
\end{align}
La (\ref{2a}) se demuestra por la siguiente cadena de desigualdades:
\begin{align}
x &≤ x ⊔ y &&\text{[por \ref{L2}]} \\
&≤ (x ⊔ y) ⊔ z &&\text{[por \ref{L2}]}
\end{align}
Para demostrar (\ref{2b}), por \ref{L4}, basta probar
\begin{align}
y &≤ (x ⊔ y) ⊔ z \tag{2b1} \label{2b1} \\
z &≤ (x ⊔ y) ⊔ z \tag{2b2} \label{2b2}
\end{align}
La (\ref{2b1}) se demuestra por la siguiente cadena de desigualdades:
\begin{align}
y &≤ x ⊔ y &&\text{[por \ref{L3}]} \\
&≤ (x ⊔ y) ⊔ z &&\text{[por \ref{L2}]}
\end{align}
La (\ref{2b2}) se tiene por \ref{L3}.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 |
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 ≤ x ⊔ (y ⊔ z) := by { have h1a1 : x ≤ x ⊔ (y ⊔ z) := by exact le_sup_left have h1a2 : y ≤ x ⊔ (y ⊔ z) := calc y ≤ y ⊔ z := by exact le_sup_left _ ≤ x ⊔ (y ⊔ z) := by exact le_sup_right show x ⊔ y ≤ x ⊔ (y ⊔ z) exact sup_le h1a1 h1a2 } have h1b : z ≤ x ⊔ (y ⊔ z) := calc z ≤ y ⊔ z := by exact le_sup_right _ ≤ x ⊔ (y ⊔ z) := by exact le_sup_right show (x ⊔ y) ⊔ z ≤ x ⊔ (y ⊔ z) exact sup_le h1a h1b } have h2 : x ⊔ (y ⊔ z) ≤ (x ⊔ y) ⊔ z := by { have h2a : x ≤ (x ⊔ y) ⊔ z := calc x ≤ x ⊔ y := by exact le_sup_left _ ≤ (x ⊔ y) ⊔ z := by exact le_sup_left have h2b : y ⊔ z ≤ (x ⊔ y) ⊔ z := by { have h2b1 : y ≤ (x ⊔ y) ⊔ z := calc y ≤ x ⊔ y := by exact le_sup_right _ ≤ (x ⊔ y) ⊔ z := by exact le_sup_left have h2b2 : z ≤ (x ⊔ y) ⊔ z := by exact le_sup_right show y ⊔ z ≤ (x ⊔ y) ⊔ z exact sup_le h2b1 h2b2 } show x ⊔ (y ⊔ z) ≤ (x ⊔ y) ⊔ z exact sup_le 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 · -- (x ⊔ y) ⊔ z ≤ x ⊔ (y ⊔ z) apply sup_le · -- x ⊔ y ≤ x ⊔ (y ⊔ z) apply sup_le . -- x ≤ x ⊔ (y ⊔ z) apply le_sup_left · -- y ≤ x ⊔ (y ⊔ z) apply le_trans . -- y ≤ y ⊔ z apply @le_sup_left _ _ y z . -- y ⊔ z ≤ x ⊔ (y ⊔ z) apply le_sup_right . -- z ≤ x ⊔ (y ⊔ z) apply le_trans . -- z ≤ x ⊔ (y ⊔ z) apply @le_sup_right _ _ y z . -- y ⊔ z ≤ x ⊔ (y ⊔ z) apply le_sup_right . -- x ⊔ (y ⊔ z) ≤ (x ⊔ y) ⊔ z apply sup_le · -- x ≤ (x ⊔ y) ⊔ z apply le_trans . -- x ≤ x ⊔ y apply @le_sup_left _ _ x y . -- x ⊔ y ≤ (x ⊔ y) ⊔ z apply le_sup_left . -- y ⊔ z ≤ (x ⊔ y) ⊔ z apply sup_le · -- y ≤ (x ⊔ y) ⊔ z apply le_trans . -- y ≤ x ⊔ y apply @le_sup_right _ _ x y . -- x ⊔ y ≤ (x ⊔ y) ⊔ z apply le_sup_left . -- z ≤ (x ⊔ y) ⊔ z apply le_sup_right -- 3ª demostración -- =============== example : x ⊔ y ⊔ z = x ⊔ (y ⊔ z) := by apply le_antisymm · apply sup_le · apply sup_le . apply le_sup_left · apply le_trans . apply @le_sup_left _ _ y z . apply le_sup_right . apply le_trans . apply @le_sup_right _ _ y z . apply le_sup_right . apply sup_le · apply le_trans . apply @le_sup_left _ _ x y . apply le_sup_left . apply sup_le · apply le_trans . apply @le_sup_right _ _ x y . apply le_sup_left . apply le_sup_right -- 4ª demostración -- =============== example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) := by apply le_antisymm . -- (x ⊔ y) ⊔ z ≤ x ⊔ (y ⊔ z) apply sup_le . -- x ⊔ y ≤ x ⊔ (y ⊔ z) apply sup_le le_sup_left (le_sup_of_le_right le_sup_left) . -- z ≤ x ⊔ (y ⊔ z) apply le_sup_of_le_right le_sup_right . -- x ⊔ (y ⊔ z) ≤ (x ⊔ y) ⊔ z apply sup_le . -- x ≤ (x ⊔ y) ⊔ z apply le_sup_of_le_left le_sup_left . -- y ⊔ z ≤ (x ⊔ y) ⊔ z apply sup_le (le_sup_of_le_left le_sup_right) le_sup_right -- 5ª demostración -- =============== example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) := by apply le_antisymm . apply sup_le . apply sup_le le_sup_left (le_sup_of_le_right le_sup_left) . apply le_sup_of_le_right le_sup_right . apply sup_le . apply le_sup_of_le_left le_sup_left . apply sup_le (le_sup_of_le_left le_sup_right) le_sup_right -- 6ª demostración -- =============== example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) := le_antisymm (sup_le (sup_le le_sup_left (le_sup_of_le_right le_sup_left)) (le_sup_of_le_right le_sup_right)) (sup_le (le_sup_of_le_left le_sup_left) (sup_le (le_sup_of_le_left le_sup_right) le_sup_right)) -- 7ª demostración -- =============== example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) := -- by apply? sup_assoc -- Lemas usados -- ============ -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) -- #check (le_sup_left : x ≤ x ⊔ y) -- #check (le_sup_of_le_left : z ≤ x → z ≤ x ⊔ y) -- #check (le_sup_of_le_right : z ≤ y → z ≤ x ⊔ y) -- #check (le_sup_right : y ≤ x ⊔ y) -- #check (le_trans : x ≤ y → y ≤ z → x ≤ z) -- #check (sup_assoc : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)) -- #check (sup_le : x ≤ z → y ≤ z → x ⊔ y ≤ 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.
