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

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

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

\nimport Mathlib.Order.Lattice\nvariable {\u03b1 : Type _} [Lattice \u03b1]\nvariable (a b c : \u03b1)\n\nexample\n  (h : \u2200 x y z : \u03b1, x \u2293 (y \u2294 z) = (x \u2293 y) \u2294 (x \u2293 z))\n  : (a \u2294 b) \u2293 c = (a \u2293 c) \u2294 (b \u2293 c) :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Se demuestra por la siguiente cadena de igualdades
\n\\begin{align}
\n   (a \u2294 b) \u2293 c &= c \u2293 (a \u2294 b)          &&\\text{[por conmutatividad de \u2293]} \\
\n               &= (c \u2293 a) \u2294 (c \u2293 b)    &&\\text{[por la hip\u00f3tesis]} \\
\n               &= (a \u2293 c) \u2294 (c \u2293 b)    &&\\text{[por conmutatividad de \u2293]} \\
\n               &= (a \u2293 c) \u2294 (b \u2293 c)    &&\\text{[por conmutatividad de \u2293]}
\n\\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Order.Lattice\nvariable {\u03b1 : Type _} [Lattice \u03b1]\nvariable (a b c : \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 x y z : \u03b1, x \u2293 (y \u2294 z) = (x \u2293 y) \u2294 (x \u2293 z))\n  : (a \u2294 b) \u2293 c = (a \u2293 c) \u2294 (b \u2293 c) :=\ncalc\n  (a \u2294 b) \u2293 c = c \u2293 (a \u2294 b)       := by rw [inf_comm]\n            _ = (c \u2293 a) \u2294 (c \u2293 b) := by rw [h]\n            _ = (a \u2293 c) \u2294 (c \u2293 b) := by rw [@inf_comm _ _ c a]\n            _ = (a \u2293 c) \u2294 (b \u2293 c) := by rw [@inf_comm _ _ c b]\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 x y z : \u03b1, x \u2293 (y \u2294 z) = (x \u2293 y) \u2294 (x \u2293 z))\n  : (a \u2294 b) \u2293 c = (a \u2293 c) \u2294 (b \u2293 c) :=\nby simp [h, inf_comm]\n\n-- Lemas usados\n-- ============\n\n-- #check (inf_comm : a \u2293 b = b \u2293 a)\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