Demostrar con Lean4 que en los ret\u00edculos se verifica que
\n\\[ (x \u2294 y) \u2294 z = x \u2294 (y \u2294 z) \\]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Order.Lattice\r\n\r\nvariable {\u03b1 : Type _} [Lattice \u03b1]\r\nvariable (x y z : \u03b1)\r\n\r\nexample : (x \u2294 y) \u2294 z = x \u2294 (y \u2294 z) :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nEn la demostraci\u00f3n se usar\u00e1n los siguientes lemas
\n\\begin{align}
\n &x \u2264 y \u2192 y \u2264 x \u2192 x = y \\tag{L1} \\label{L1} \\\\
\n &x \u2264 x \u2294 y \\tag{L2} \\label{L2} \\\\
\n &y \u2264 x \u2294 y \\tag{L3} \\label{L3} \\\\
\n &x \u2264 z \u2192 y \u2264 z \u2192 x \u2294 y \u2264 z \\tag{L4} \\label{L4} \\\\
\n\\end{align}<\/p>\n
Por \\ref{L1}, basta demostrar las siguientes relaciones:
\n\\begin{align}
\n (x \u2294 y) \u2294 z &\u2264 x \u2294 (y \u2294 z) \\tag{1} \\label{1} \\\\
\n x \u2294 (y \u2294 z) &\u2264 (x \u2294 y) \u2294 z \\tag{2} \\label{2}
\n\\end{align}<\/p>\n
Para demostrar (\\ref{1}), por \\ref{L4}, basta probar
\n\\begin{align}
\n x \u2294 y &\u2264 x \u2294 (y \u2294 z) \\tag{1a} \\label{1a} \\\\
\n z &\u2264 x \u2294 (y \u2294 z) \\tag{1b} \\label{1b}
\n\\end{align}<\/p>\n
Para demostrar (\\ref{1a}), por \\ref{L4}, basta probar
\n\\begin{align}
\n x &\u2264 x \u2294 (y \u2294 z) \\tag{1a1} \\label{1a1} \\\\
\n y &\u2264 x \u2294 (y \u2294 z) \\tag{1a2} \\label{1a2}
\n\\end{align}<\/p>\n
La (\\ref{1a1}) se tiene por \\ref{L2}.<\/p>\n
La (\\ref{1a2}) se tiene por la siguiente cadena de desigualdades:
\n\\begin{align}
\n y &\u2264 y \u2294 z &&\\text{[por \\ref{L2}]} \\\\
\n &\u2264 x \u2294 (y \u2294 z) &&\\text{[por \\ref{L3}]}
\n\\end{align}<\/p>\n
La (\\ref{1b}) se tiene por la siguiente cadena de desigualdades
\n\\begin{align}
\n z &\u2264 y \u2294 z &&\\text{[por \\ref{L3}]} \\\\
\n &\u2264 x \u2294 (y \u2294 z) &&\\text{[por \\ref{L3}]}
\n\\end{align}<\/p>\n
Para demostrar (\\ref{2}), por \\ref{L4}, basta probar
\n\\begin{align}
\n x &\u2264 (x \u2294 y) \u2294 z \\tag{2a} \\label{2a} \\\\
\n y \u2294 z &\u2264 (x \u2294 y) \u2294 z \\tag{2b} \\label{2b}
\n\\end{align}<\/p>\n
La (\\ref{2a}) se demuestra por la siguiente cadena de desigualdades:
\n\\begin{align}
\n x &\u2264 x \u2294 y &&\\text{[por \\ref{L2}]} \\\\
\n &\u2264 (x \u2294 y) \u2294 z &&\\text{[por \\ref{L2}]}
\n\\end{align}<\/p>\n
Para demostrar (\\ref{2b}), por \\ref{L4}, basta probar
\n\\begin{align}
\n y &\u2264 (x \u2294 y) \u2294 z \\tag{2b1} \\label{2b1} \\\\
\n z &\u2264 (x \u2294 y) \u2294 z \\tag{2b2} \\label{2b2}
\n\\end{align}<\/p>\n
La (\\ref{2b1}) se demuestra por la siguiente cadena de desigualdades:
\n\\begin{align}
\n y &\u2264 x \u2294 y &&\\text{[por \\ref{L3}]} \\\\
\n &\u2264 (x \u2294 y) \u2294 z &&\\text{[por \\ref{L2}]}
\n\\end{align}<\/p>\n
La (\\ref{2b2}) se tiene por \\ref{L3}.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Order.Lattice\r\n\r\nvariable {\u03b1 : Type _} [Lattice \u03b1]\r\nvariable (x y z : \u03b1)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : (x \u2294 y) \u2294 z = x \u2294 (y \u2294 z) :=\r\nby\r\n have h1 : (x \u2294 y) \u2294 z \u2264 x \u2294 (y \u2294 z) := by\r\n { have h1a : x \u2294 y \u2264 x \u2294 (y \u2294 z) := by\r\n { have h1a1 : x \u2264 x \u2294 (y \u2294 z) := by exact le_sup_left\r\n have h1a2 : y \u2264 x \u2294 (y \u2294 z) := calc\r\n y \u2264 y \u2294 z := by exact le_sup_left\r\n _ \u2264 x \u2294 (y \u2294 z) := by exact le_sup_right\r\n show x \u2294 y \u2264 x \u2294 (y \u2294 z)\r\n exact sup_le h1a1 h1a2 }\r\n have h1b : z \u2264 x \u2294 (y \u2294 z) := calc\r\n z \u2264 y \u2294 z := by exact le_sup_right\r\n _ \u2264 x \u2294 (y \u2294 z) := by exact le_sup_right\r\n show (x \u2294 y) \u2294 z \u2264 x \u2294 (y \u2294 z)\r\n exact sup_le h1a h1b }\r\n have h2 : x \u2294 (y \u2294 z) \u2264 (x \u2294 y) \u2294 z := by\r\n { have h2a : x \u2264 (x \u2294 y) \u2294 z := calc\r\n x \u2264 x \u2294 y := by exact le_sup_left\r\n _ \u2264 (x \u2294 y) \u2294 z := by exact le_sup_left\r\n have h2b : y \u2294 z \u2264 (x \u2294 y) \u2294 z := by\r\n { have h2b1 : y \u2264 (x \u2294 y) \u2294 z := calc\r\n y \u2264 x \u2294 y := by exact le_sup_right\r\n _ \u2264 (x \u2294 y) \u2294 z := by exact le_sup_left\r\n have h2b2 : z \u2264 (x \u2294 y) \u2294 z := by\r\n exact le_sup_right\r\n show y \u2294 z \u2264 (x \u2294 y) \u2294 z\r\n exact sup_le h2b1 h2b2 }\r\n show x \u2294 (y \u2294 z) \u2264 (x \u2294 y) \u2294 z\r\n exact sup_le h2a h2b }\r\n show (x \u2294 y) \u2294 z = x \u2294 (y \u2294 z)\r\n exact le_antisymm h1 h2\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : x \u2294 y \u2294 z = x \u2294 (y \u2294 z) :=\r\nby\r\n apply le_antisymm\r\n \u00b7 -- (x \u2294 y) \u2294 z \u2264 x \u2294 (y \u2294 z)\r\n apply sup_le\r\n \u00b7 -- x \u2294 y \u2264 x \u2294 (y \u2294 z)\r\n apply sup_le\r\n . -- x \u2264 x \u2294 (y \u2294 z)\r\n apply le_sup_left\r\n \u00b7 -- y \u2264 x \u2294 (y \u2294 z)\r\n apply le_trans\r\n . -- y \u2264 y \u2294 z\r\n apply @le_sup_left _ _ y z\r\n . -- y \u2294 z \u2264 x \u2294 (y \u2294 z)\r\n apply le_sup_right\r\n . -- z \u2264 x \u2294 (y \u2294 z)\r\n apply le_trans\r\n . -- z \u2264 x \u2294 (y \u2294 z)\r\n apply @le_sup_right _ _ y z\r\n . -- y \u2294 z \u2264 x \u2294 (y \u2294 z)\r\n apply le_sup_right\r\n . -- x \u2294 (y \u2294 z) \u2264 (x \u2294 y) \u2294 z\r\n apply sup_le\r\n \u00b7 -- x \u2264 (x \u2294 y) \u2294 z\r\n apply le_trans\r\n . -- x \u2264 x \u2294 y\r\n apply @le_sup_left _ _ x y\r\n . -- x \u2294 y \u2264 (x \u2294 y) \u2294 z\r\n apply le_sup_left\r\n . -- y \u2294 z \u2264 (x \u2294 y) \u2294 z\r\n apply sup_le\r\n \u00b7 -- y \u2264 (x \u2294 y) \u2294 z\r\n apply le_trans\r\n . -- y \u2264 x \u2294 y\r\n apply @le_sup_right _ _ x y\r\n . -- x \u2294 y \u2264 (x \u2294 y) \u2294 z\r\n apply le_sup_left\r\n . -- z \u2264 (x \u2294 y) \u2294 z\r\n apply le_sup_right\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : x \u2294 y \u2294 z = x \u2294 (y \u2294 z) :=\r\nby\r\n apply le_antisymm\r\n \u00b7 apply sup_le\r\n \u00b7 apply sup_le\r\n . apply le_sup_left\r\n \u00b7 apply le_trans\r\n . apply @le_sup_left _ _ y z\r\n . apply le_sup_right\r\n . apply le_trans\r\n . apply @le_sup_right _ _ y z\r\n . apply le_sup_right\r\n . apply sup_le\r\n \u00b7 apply le_trans\r\n . apply @le_sup_left _ _ x y\r\n . apply le_sup_left\r\n . apply sup_le\r\n \u00b7 apply le_trans\r\n . apply @le_sup_right _ _ x y\r\n . apply le_sup_left\r\n . apply le_sup_right\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : (x \u2294 y) \u2294 z = x \u2294 (y \u2294 z) :=\r\nby\r\n apply le_antisymm\r\n . -- (x \u2294 y) \u2294 z \u2264 x \u2294 (y \u2294 z)\r\n apply sup_le\r\n . -- x \u2294 y \u2264 x \u2294 (y \u2294 z)\r\n apply sup_le le_sup_left (le_sup_of_le_right le_sup_left)\r\n . -- z \u2264 x \u2294 (y \u2294 z)\r\n apply le_sup_of_le_right le_sup_right\r\n . -- x \u2294 (y \u2294 z) \u2264 (x \u2294 y) \u2294 z\r\n apply sup_le\r\n . -- x \u2264 (x \u2294 y) \u2294 z\r\n apply le_sup_of_le_left le_sup_left\r\n . -- y \u2294 z \u2264 (x \u2294 y) \u2294 z\r\n apply sup_le (le_sup_of_le_left le_sup_right) le_sup_right\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : (x \u2294 y) \u2294 z = x \u2294 (y \u2294 z) :=\r\nby\r\n apply le_antisymm\r\n . apply sup_le\r\n . apply sup_le le_sup_left (le_sup_of_le_right le_sup_left)\r\n . apply le_sup_of_le_right le_sup_right\r\n . apply sup_le\r\n . apply le_sup_of_le_left le_sup_left\r\n . apply sup_le (le_sup_of_le_left le_sup_right) le_sup_right\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : (x \u2294 y) \u2294 z = x \u2294 (y \u2294 z) :=\r\nle_antisymm\r\n (sup_le\r\n (sup_le le_sup_left (le_sup_of_le_right le_sup_left))\r\n (le_sup_of_le_right le_sup_right))\r\n (sup_le\r\n (le_sup_of_le_left le_sup_left)\r\n (sup_le (le_sup_of_le_left le_sup_right) le_sup_right))\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : (x \u2294 y) \u2294 z = x \u2294 (y \u2294 z) :=\r\n-- by apply?\r\nsup_assoc\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- #check (le_antisymm : x \u2264 y \u2192 y \u2264 x \u2192 x = y)\r\n-- #check (le_sup_left : x \u2264 x \u2294 y)\r\n-- #check (le_sup_of_le_left : z \u2264 x \u2192 z \u2264 x \u2294 y)\r\n-- #check (le_sup_of_le_right : z \u2264 y \u2192 z \u2264 x \u2294 y)\r\n-- #check (le_sup_right : y \u2264 x \u2294 y)\r\n-- #check (le_trans : x \u2264 y \u2192 y \u2264 z \u2192 x \u2264 z)\r\n-- #check (sup_assoc : (x \u2294 y) \u2294 z = x \u2294 (y \u2294 z))\r\n-- #check (sup_le : x \u2264 z \u2192 y \u2264 z \u2192 x \u2294 y \u2264 z)\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n