La semana en Calculemus (23 de septiembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. En los retículos, x ⊔ y = y ⊔ x
- 2. En los retículos, (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)
- 3. En los retículos, (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)
- 4. En los retículos, x ⊓ (x ⊔ y) = x
- 5. En los retículos, x ⊔ (x ⊓ y) = x
A continuación se muestran las soluciones.
1. 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 |
Demostración en lenguaje natural
Es consecuencia del siguiente lema auxiliar
\[ (∀ a, b)[a ⊔ b ≤ b ⊔ a] \tag{1} \]
En efecto, sustituyendo en (1) \(a\) por \(x\) y \(b\) por \(y\), se tiene
\[ x ⊔ y ≤ y ⊔ x \tag{2} \]
y sustituyendo en (1) \(a\) por \(y\) y \(b\) por \(x\), se tiene
\[ y ⊔ x ≤ x ⊔ y \tag{3} \]
Finalmente, aplicando la propiedad antisimétrica de la divisibilidad
a (2) y (3), se tiene
\[ x ⊔ y = y ⊔ x \]
Para demostrar (1), por la definición del supremo, basta demostrar las siguientes relaciones
\begin{align}
x &≤ y ⊔ x \\
y &≤ y ⊔ x
\end{align}
y ambas se tienen por la definición del supremo.
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 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y z : α) -- 1ª demostración del lema auxiliar lemma aux : x ⊔ y ≤ y ⊔ x := by have h1 : x ≤ y ⊔ x := le_sup_right have h2 : y ≤ y ⊔ x := le_sup_left show x ⊔ y ≤ y ⊔ x exact sup_le h1 h2 -- 2ª demostración del lema auxiliar example : x ⊔ y ≤ y ⊔ x := by apply sup_le { apply le_sup_right } { apply le_sup_left } -- 3ª demostración del lema auxiliar example : x ⊔ y ≤ y ⊔ x := sup_le le_sup_right le_sup_left -- 1ª demostración example : x ⊔ y = y ⊔ x := by have h1 : x ⊔ y ≤ y ⊔ x := aux x y have h2 : y ⊔ x ≤ x ⊔ y := aux y x show x ⊔ y = y ⊔ x exact le_antisymm h1 h2 -- 2ª demostración example : x ⊔ y = y ⊔ x := by apply le_antisymm { apply aux } { apply aux } -- 3ª demostración example : x ⊔ y = y ⊔ x := le_antisymm (aux x y) (aux y x) -- 4ª demostración example : x ⊔ y = y ⊔ x := by apply le_antisymm; simp ; simp -- 5ª demostración example : x ⊔ y = y ⊔ x := -- by apply? sup_comm -- Lemas usados -- ============ -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) -- #check (le_sup_left : x ≤ x ⊔ y) -- #check (le_sup_right : y ≤ x ⊔ y) -- #check (sup_comm : x ⊔ y = y ⊔ x) -- #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. 20.
2. 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 |
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
|
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 |
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 -- Lemas usados -- ============ -- #check (inf_assoc : (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.
3. 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.
4. 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 |
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} \\
&x ⊓ y ≤ x \tag{L2} \\
&z ≤ x → z ≤ y → z ≤ x ⊓ y \tag{L3} \\
&x ≤ x \tag{L4} \\
&x ≤ x ⊔ y \tag{L5} \\
\end{align}
Por L1, basta demostrar las siguientes relaciones:
\begin{align}
&x ⊓ (x ⊔ y) ≤ x \tag{1} \\
&x ≤ x ⊓ (x ⊔ y) \tag{2}
\end{align}
La (1) se tiene por L2.
Para demostrar la (2), por L3, basta probar las relaciones:
\begin{align}
x &≤ x \tag{2a} \\
x &≤ x ⊔ y \tag{2b}
\end{align}
La (2a) se tiene por L4.
La (2b) se tiene por L5
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 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y : α) -- 1ª demostración -- =============== example : x ⊓ (x ⊔ y) = x := by have h1 : x ⊓ (x ⊔ y) ≤ x := inf_le_left have h2 : x ≤ x ⊓ (x ⊔ y) { have h2a : x ≤ x := le_rfl have h2b : x ≤ x ⊔ y := le_sup_left show x ≤ x ⊓ (x ⊔ y) exact le_inf h2a h2b } show x ⊓ (x ⊔ y) = x exact le_antisymm h1 h2 -- 2ª demostración -- =============== example : x ⊓ (x ⊔ y) = x := by have h1 : x ⊓ (x ⊔ y) ≤ x := by simp have h2 : x ≤ x ⊓ (x ⊔ y) := by simp show x ⊓ (x ⊔ y) = x exact le_antisymm h1 h2 -- 3ª demostración -- =============== example : x ⊓ (x ⊔ y) = x := by apply le_antisymm . -- x ⊓ (x ⊔ y) ≤ x apply inf_le_left . -- x ≤ x ⊓ (x ⊔ y) apply le_inf . -- x ≤ x apply le_rfl . -- x ≤ x ⊔ y apply le_sup_left -- 4ª demostración -- =============== example : x ⊓ (x ⊔ y) = x := le_antisymm inf_le_left (le_inf le_rfl le_sup_left) -- 5ª demostración -- =============== example : x ⊓ (x ⊔ y) = x := -- by apply? inf_sup_self -- 6ª demostración -- =============== example : x ⊓ (x ⊔ y) = x := by simp -- Lemas usados -- ============ -- variable (z : α) -- #check (inf_le_left : x ⊓ y ≤ x) -- #check (inf_sup_self : x ⊓ (x ⊔ y) = x) -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) -- #check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y) -- #check (le_rfl : x ≤ x) -- #check (le_sup_left : x ≤ x ⊔ y) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 21.
5. 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 |
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} \\
&x ⊓ y ≤ x \tag{L2} \\
&x ≤ x \tag{L3} \\
&x ≤ x ⊔ y \tag{L4} \\
&x ≤ z → y ≤ z → x ⊔ y ≤ z \tag{L5}
\end{align}
Por L1, basta demostrar las siguientes relaciones:
\begin{align}
&x ⊔ (x ⊓ y) ≤ x \tag{1} \\
&x ≤ x ⊔ (x ⊓ y) &&\text{[que se tiene por L4]}
\end{align}
Para demostrar (1), por L5, basta probar las relaciones:
\begin{align}
&x ≤ x &&\text{[que se tiene por L3]} \\
&x ⊓ y ≤ x &&\text{[que se tiene por L2]}
\end{align}
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 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α]-- variable (x y : α) -- 1ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := by have h1 : x ⊔ (x ⊓ y) ≤ x { have h1a : x ≤ x := le_rfl have h1b : x ⊓ y ≤ x := inf_le_left show x ⊔ (x ⊓ y) ≤ x exact sup_le h1a h1b } have h2 : x ≤ x ⊔ (x ⊓ y) := le_sup_left show x ⊔ (x ⊓ y) = x exact le_antisymm h1 h2 -- 2ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := by have h1 : x ⊔ (x ⊓ y) ≤ x := by simp have h2 : x ≤ x ⊔ (x ⊓ y) := by simp show x ⊔ (x ⊓ y) = x exact le_antisymm h1 h2 -- 3ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := by apply le_antisymm . -- x ⊔ (x ⊓ y) ≤ x apply sup_le . -- x ≤ x apply le_rfl . -- x ⊓ y ≤ x apply inf_le_left . -- x ≤ x ⊔ (x ⊓ y) apply le_sup_left -- 4ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := -- by apply? sup_inf_self -- 5ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := by simp -- Lemas usados -- ============ -- variable (z : α) -- #check (le_rfl : x ≤ x) -- #check (inf_le_left : x ⊓ y ≤ x) -- #check (sup_le : x ≤ z → y ≤ z → x ⊔ y ≤ z) -- #check (le_sup_left : x ≤ x ⊔ y) -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) -- #check (sup_inf_self : x ⊔ (x ⊓ y) = x) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 21.