Demostrar con Lean4 que en los ret\u00edculos se verifica que
\n\\[x \u2294 y = y \u2294 x\\]
\npara todo \\(x\\) e \\(y\\) en el 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 (x y z : \u03b1)\r\n\r\nexample : x \u2294 y = y \u2294 x :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nEs consecuencia del siguiente lema auxiliar
\n\\[ (\u2200 a, b)[a \u2294 b \u2264 b \u2294 a] \\tag{1} \\]
\nEn efecto, sustituyendo en (1) \\(a\\) por \\(x\\) y \\(b\\) por \\(y\\), se tiene
\n\\[ x \u2294 y \u2264 y \u2294 x \\tag{2} \\]
\ny sustituyendo en (1) \\(a\\) por \\(y\\) y \\(b\\) por \\(x\\), se tiene
\n\\[ y \u2294 x \u2264 x \u2294 y \\tag{3} \\]
\nFinalmente, aplicando la propiedad antisim\u00e9trica de la divisibilidad
\na (2) y (3), se tiene
\n\\[ x \u2294 y = y \u2294 x \\]<\/p>\n
Para demostrar (1), por la definici\u00f3n del supremo, basta demostrar las siguientes relaciones
\n\\begin{align}
\n x &\u2264 y \u2294 x \\\\
\n y &\u2264 y \u2294 x
\n\\end{align}
\ny ambas se tienen por la definici\u00f3n del supremo.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Order.Lattice\r\nvariable {\u03b1 : Type _} [Lattice \u03b1]\r\nvariable (x y z : \u03b1)\r\n\r\n-- 1\u00aa demostraci\u00f3n del lema auxiliar\r\nlemma aux : x \u2294 y \u2264 y \u2294 x :=\r\nby\r\n have h1 : x \u2264 y \u2294 x :=\r\n le_sup_right\r\n have h2 : y \u2264 y \u2294 x :=\r\n le_sup_left\r\n show x \u2294 y \u2264 y \u2294 x\r\n exact sup_le h1 h2\r\n\r\n-- 2\u00aa demostraci\u00f3n del lema auxiliar\r\nexample : x \u2294 y \u2264 y \u2294 x :=\r\nby\r\n apply sup_le\r\n { apply le_sup_right }\r\n { apply le_sup_left }\r\n\r\n-- 3\u00aa demostraci\u00f3n del lema auxiliar\r\nexample : x \u2294 y \u2264 y \u2294 x :=\r\nsup_le le_sup_right le_sup_left\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : x \u2294 y = y \u2294 x :=\r\nby\r\n have h1 : x \u2294 y \u2264 y \u2294 x :=\r\n aux x y\r\n have h2 : y \u2294 x \u2264 x \u2294 y :=\r\n aux y x\r\n show x \u2294 y = y \u2294 x\r\n exact le_antisymm h1 h2\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : x \u2294 y = y \u2294 x :=\r\nby\r\n apply le_antisymm\r\n { apply aux }\r\n { apply aux }\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : x \u2294 y = y \u2294 x :=\r\nle_antisymm (aux x y) (aux y x)\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample : x \u2294 y = y \u2294 x :=\r\nby apply le_antisymm; simp ; simp\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample : x \u2294 y = y \u2294 x :=\r\n-- by apply?\r\nsup_comm\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_right : y \u2264 x \u2294 y)\r\n-- #check (sup_comm : x \u2294 y = y \u2294 x)\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