Demostrar con Lean4 que en los ret\u00edculos se verifica que
\n\\[ x \u2293 (x \u2294 y) = x \\]<\/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 : \u03b1)\r\n\r\nexample : x \u2293 (x \u2294 y) = x :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nEn la demostraci\u00f3n se usar\u00e1n los siguientes lemas
\n\\begin{align}
\n &x \u2264 y \u2192 y \u2264 x \u2192 x = y \\tag{L1} \\\\
\n &x \u2293 y \u2264 x \\tag{L2} \\\\
\n &z \u2264 x \u2192 z \u2264 y \u2192 z \u2264 x \u2293 y \\tag{L3} \\\\
\n &x \u2264 x \\tag{L4} \\\\
\n &x \u2264 x \u2294 y \\tag{L5} \\\\
\n\\end{align}<\/p>\n
Por L1, basta demostrar las siguientes relaciones:
\n\\begin{align}
\n &x \u2293 (x \u2294 y) \u2264 x \\tag{1} \\\\
\n &x \u2264 x \u2293 (x \u2294 y) \\tag{2}
\n\\end{align}<\/p>\n
La (1) se tiene por L2.<\/p>\n
Para demostrar la (2), por L3, basta probar las relaciones:
\n\\begin{align}
\n x &\u2264 x \\tag{2a} \\\\
\n x &\u2264 x \u2294 y \\tag{2b}
\n\\end{align}<\/p>\n
La (2a) se tiene por L4.<\/p>\n
La (2b) se tiene por L5<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Order.Lattice\r\nvariable {\u03b1 : Type _} [Lattice \u03b1]\r\nvariable (x y : \u03b1)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : x \u2293 (x \u2294 y) = x :=\r\nby\r\n have h1 : x \u2293 (x \u2294 y) \u2264 x := inf_le_left\r\n have h2 : x \u2264 x \u2293 (x \u2294 y)\r\n { have h2a : x \u2264 x := le_rfl\r\n have h2b : x \u2264 x \u2294 y := le_sup_left\r\n show x \u2264 x \u2293 (x \u2294 y)\r\n exact le_inf h2a h2b }\r\n show x \u2293 (x \u2294 y) = x\r\n exact le_antisymm h1 h2\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : x \u2293 (x \u2294 y) = x :=\r\nby\r\n have h1 : x \u2293 (x \u2294 y) \u2264 x := by simp\r\n have h2 : x \u2264 x \u2293 (x \u2294 y) := by simp\r\n show x \u2293 (x \u2294 y) = x\r\n exact le_antisymm h1 h2\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : x \u2293 (x \u2294 y) = x :=\r\nby\r\n apply le_antisymm\r\n . -- x \u2293 (x \u2294 y) \u2264 x\r\n apply inf_le_left\r\n . -- x \u2264 x \u2293 (x \u2294 y)\r\n apply le_inf\r\n . -- x \u2264 x\r\n apply le_rfl\r\n . -- x \u2264 x \u2294 y\r\n apply le_sup_left\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : x \u2293 (x \u2294 y) = x :=\r\nle_antisymm inf_le_left (le_inf le_rfl le_sup_left)\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : x \u2293 (x \u2294 y) = x :=\r\n-- by apply?\r\ninf_sup_self\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : x \u2293 (x \u2294 y) = x :=\r\nby simp\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- variable (z : \u03b1)\r\n-- #check (inf_le_left : x \u2293 y \u2264 x)\r\n-- #check (inf_sup_self : x \u2293 (x \u2294 y) = x)\r\n-- #check (le_antisymm : x \u2264 y \u2192 y \u2264 x \u2192 x = y)\r\n-- #check (le_inf : z \u2264 x \u2192 z \u2264 y \u2192 z \u2264 x \u2293 y)\r\n-- #check (le_rfl : x \u2264 x)\r\n-- #check (le_sup_left : x \u2264 x \u2294 y)\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