{"id":1598,"date":"2023-09-26T06:00:04","date_gmt":"2023-09-26T04:00:04","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1598"},"modified":"2023-09-07T11:01:25","modified_gmt":"2023-09-07T09:01:25","slug":"26-sep-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/26-sep-23\/","title":{"rendered":"En los ret\u00edculos, una distributiva del supremo implica la otra"},"content":{"rendered":"

Demostrar con Lean4 que si \\(R\\) es un ret\u00edculo tal que
\n\\[ (\u2200 x,\\ y,\\ z \\in R) [x \u2294 (y \u2293 z) = (x \u2294 y) \u2293 (x \u2294 z)] \\]
\nentonces
\n\\[ (a \u2293 b) \u2294 c = (a \u2294 c) \u2293 (b \u2294 c) \\]
\npara todos los elementos del ret\u00edculo.<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n

\r\nimport Mathlib.Order.Lattice\r\nvariable {\u03b1 : Type _} [Lattice \u03b1]\r\nvariable (a b c : \u03b1)\r\n\r\nexample\r\n  (h : \u2200 x y z : \u03b1, x \u2294 (y \u2293 z) = (x \u2294 y) \u2293 (x \u2294 z))\r\n  : (a \u2293 b) \u2294 c = (a \u2294 c) \u2293 (b \u2294 c) :=\r\nby sorry\r\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nSe demuestra por la siguiente cadena de igualdades
\n\\begin{align}
\n   (a \u2293 b) \u2294 c &= c \u2294 (a \u2293 b)          &&\\text{[por la conmutatividad de \u2294]} \\\\
\n               &= (c \u2294 a) \u2293 (c \u2294 b)    &&\\text{[por la hip\u00f3tesis]} \\\\
\n               &= (a \u2294 c) \u2293 (c \u2294 b)    &&\\text{[por la conmutatividad de \u2294]} \\\\
\n               &= (a \u2294 c) \u2293 (b \u2294 c)    &&\\text{[por la conmutatividad de \u2294]}
\n\\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\r\nimport Mathlib.Order.Lattice\r\nvariable {\u03b1 : Type _} [Lattice \u03b1]\r\nvariable (a b c : \u03b1)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n  (h : \u2200 x y z : \u03b1, x \u2294 (y \u2293 z) = (x \u2294 y) \u2293 (x \u2294 z))\r\n  : (a \u2293 b) \u2294 c = (a \u2294 c) \u2293 (b \u2294 c) :=\r\ncalc\r\n  (a \u2293 b) \u2294 c = c \u2294 (a \u2293 b)       := by rw [sup_comm]\r\n            _ = (c \u2294 a) \u2293 (c \u2294 b) := by rw [h]\r\n            _ = (a \u2294 c) \u2293 (c \u2294 b) := by rw [@sup_comm _ _ c a]\r\n            _ = (a \u2294 c) \u2293 (b \u2294 c) := by rw [@sup_comm _ _ c b]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  (h : \u2200 x y z : \u03b1, x \u2294 (y \u2293 z) = (x \u2294 y) \u2293 (x \u2294 z))\r\n  : (a \u2293 b) \u2294 c = (a \u2294 c) \u2293 (b \u2294 c) :=\r\nby simp [h, sup_comm]\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- #check (sup_comm : a \u2294 b = b \u2294 a)\r\n<\/pre>\n
Demostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/b><\/p>\n