{"id":1135,"date":"2022-10-18T18:31:21","date_gmt":"2022-10-18T16:31:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1135"},"modified":"2022-10-18T18:31:21","modified_gmt":"2022-10-18T16:31:21","slug":"si-r-es-un-reticulo-y-x-y-z-%e2%88%88-r-entonces-x-%e2%8a%93-y-%e2%8a%93-z-x-%e2%8a%93-y-%e2%8a%93-z","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/si-r-es-un-reticulo-y-x-y-z-%e2%88%88-r-entonces-x-%e2%8a%93-y-%e2%8a%93-z-x-%e2%8a%93-y-%e2%8a%93-z\/","title":{"rendered":"Si R es un ret\u00edculo y x, y, z \u2208 R, entonces (x \u2293 y) \u2293 z = x \u2293 (y \u2293 z)"},"content":{"rendered":"

Demostrar que si R es un ret\u00edculo y x, y, z \u2208 R, entonces<\/p>\n

\n(x \u2293 y) \u2293 z = x \u2293 (y \u2293 z)\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport order.lattice\n\nvariables {R : Type*} [lattice R]\nvariables x y z : R\n\nexample : (x \u2293 y) \u2293 z = x \u2293 (y \u2293 z) :=\nsorry\n<\/pre>\n
<\/p>\n
Soluciones con Lean<\/b><\/p>\n
\nimport order.lattice\n\nvariables {R : Type*} [lattice R]\nvariables x y z : R\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (x \u2293 y) \u2293 z = x \u2293 (y \u2293 z) :=\nbegin\n  have h1 : (x \u2293 y) \u2293 z \u2264 x \u2293 (y \u2293 z),\n    { have h1a : (x \u2293 y) \u2293 z \u2264 x, calc\n        (x \u2293 y) \u2293 z \u2264 x \u2293 y : inf_le_left\n                ... \u2264 x     : inf_le_left,\n      have h1b : (x \u2293 y) \u2293 z \u2264 y \u2293 z,\n        { have h1b1 : (x \u2293 y) \u2293 z \u2264 y, calc\n            (x \u2293 y) \u2293 z \u2264 x \u2293 y : inf_le_left\n                    ... \u2264 y     : inf_le_right,\n          have h1b2 : (x \u2293 y) \u2293 z \u2264 z :=\n            inf_le_right,\n          show (x \u2293 y) \u2293 z \u2264 y \u2293 z,\n            by exact le_inf h1b1 h1b2, },\n      show (x \u2293 y) \u2293 z \u2264 x \u2293 (y \u2293 z),\n        by exact le_inf h1a h1b, },\n  have h2 : x \u2293 (y \u2293 z) \u2264 (x \u2293 y) \u2293 z,\n    { have h2a : x \u2293 (y \u2293 z) \u2264 x \u2293 y,\n        { have h2a1 : x \u2293 (y \u2293 z) \u2264 x,\n            by exact inf_le_left,\n          have h2a2 : x \u2293 (y \u2293 z) \u2264 y, calc\n            x \u2293 (y \u2293 z) \u2264 y \u2293 z : inf_le_right\n                    ... \u2264 y     : inf_le_left,\n          show x \u2293 (y \u2293 z) \u2264 x \u2293 y,\n            by exact le_inf h2a1 h2a2, },\n      have h2b : x \u2293 (y \u2293 z) \u2264 z, calc\n        x \u2293 (y \u2293 z) \u2264 y \u2293 z : inf_le_right\n                ... \u2264 z     : inf_le_right,\n      show x \u2293 (y \u2293 z) \u2264 (x \u2293 y) \u2293 z,\n        by exact le_inf h2a h2b, },\n  show (x \u2293 y) \u2293 z = x \u2293 (y \u2293 z),\n    by exact le_antisymm h1 h2,\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (x \u2293 y) \u2293 z = x \u2293 (y \u2293 z) :=\nbegin\n  apply le_antisymm,\n  { apply le_inf,\n    { apply inf_le_of_left_le inf_le_left, },\n    { apply le_inf (inf_le_of_left_le inf_le_right) inf_le_right}},\n  {apply le_inf,\n    { apply le_inf inf_le_left (inf_le_of_right_le inf_le_left), },\n    { apply inf_le_of_right_le inf_le_right, },},\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (x \u2293 y) \u2293 z = x \u2293 (y \u2293 z) :=\nle_antisymm\n  (le_inf\n    (inf_le_of_left_le inf_le_left)\n    (le_inf (inf_le_of_left_le inf_le_right) inf_le_right))\n  (le_inf\n    (le_inf inf_le_left (inf_le_of_right_le inf_le_left))\n    (inf_le_of_right_le inf_le_right))\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (x \u2293 y) \u2293 z = x \u2293 (y \u2293 z) :=\n-- by library_search\ninf_assoc\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (x \u2293 y) \u2293 z = x \u2293 (y \u2293 z) :=\n-- by hint\nby finish\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
Referencias<\/b><\/p>\n