{"id":1129,"date":"2022-10-12T06:00:09","date_gmt":"2022-10-12T04:00:09","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1129"},"modified":"2022-10-05T12:56:02","modified_gmt":"2022-10-05T10:56:02","slug":"si-r-es-un-reticulo-y-x-y-%e2%88%88-r-entonces-x-%e2%8a%93-y-y-%e2%8a%93-x","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/si-r-es-un-reticulo-y-x-y-%e2%88%88-r-entonces-x-%e2%8a%93-y-y-%e2%8a%93-x\/","title":{"rendered":"Si R es un ret\u00edculo y x, y \u2208 R, entonces x \u2293 y = y \u2293 x"},"content":{"rendered":"

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

\n    x \u2293 y = y \u2293 x\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 : R\n\nexample : x \u2293 y = y \u2293 x :=\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\nlemma aux1 : x \u2293 y \u2264 y \u2293 x :=\nbegin\n  have h1 : x \u2293 y \u2264 y,\n    by exact inf_le_right,\n  have h2 : x \u2293 y \u2264 x,\n    by exact inf_le_left,\n  show x \u2293 y \u2264 y \u2293 x,\n    by exact le_inf h1 h2,\nend\n\nexample : x \u2293 y = y \u2293 x :=\nbegin\n  have h1 : x \u2293 y \u2264 y \u2293 x,\n    by exact aux1 x y,\n  have h2 : y \u2293 x \u2264 x \u2293 y,\n    by exact aux1 y x,\n  show x \u2293 y = y \u2293 x,\n    by exact le_antisymm h1 h2,\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nlemma aux2 : x \u2293 y \u2264 y \u2293 x :=\nle_inf inf_le_right inf_le_left\n\nexample : x \u2293 y = y \u2293 x :=\nle_antisymm (aux2 x y) (aux2 y x)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nlemma aux3 : x \u2293 y \u2264 y \u2293 x :=\nbegin\n  apply le_inf,\n  apply inf_le_right,\n  apply inf_le_left,\nend\n\nexample : x \u2293 y = y \u2293 x :=\nbegin\n  apply le_antisymm,\n  apply aux3,\n  apply aux3,\nend\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2293 y = y \u2293 x :=\nby apply le_antisymm; simp\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2293 y = y \u2293 x :=\ninf_comm\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
Referencias<\/b><\/p>\n