{"id":1852,"date":"2023-12-12T06:00:04","date_gmt":"2023-12-12T04:00:04","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1852"},"modified":"2023-12-07T14:21:54","modified_gmt":"2023-12-07T12:21:54","slug":"12-dic-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/12-dic-23\/","title":{"rendered":"x \u2264 y \u2227 x \u2260 y \u22a2 y \u2270 x"},"content":{"rendered":"\n

Demostrar con Lean4 que
\n\[x \u2264 y \u2227 x \u2260 y \u22a2 y \u2270 x\]<\/p>\n

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

\nimport Mathlib.Data.Real.Basic\n\nvariable {x y : \u211d}\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Supongamos que \(y \u2264 x\). Entonces, por la antisimetr\u00eda y la primera parte de la hip\u00f3tesis, se tiene que \(x = y\) que contradice la segunda parte de la hip\u00f3tesis.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Data.Real.Basic\n\nvariable {x y : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nby\n  intro h1\n  cases' h with h2 h3\n  -- h2 : x \u2264 y\n  -- h3 : x \u2260 y\n  have h4 : x = y := le_antisymm h2 h1\n  show False\n  exact h3 h4\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nby\n  intro h1\n  have h4 : x = y := le_antisymm h.1 h1\n  show False\n  exact h.2 h4\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nby\n  intro h1\n  show False\n  exact h.2 (le_antisymm h.1 h1)\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nfun h1 \u21a6 h.2 (le_antisymm h.1 h1)\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nby\n  intro h'\n  -- h' : y \u2264 x\n  -- \u22a2 False\n  apply h.right\n  -- \u22a2 x = y\n  exact le_antisymm h.left h'\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nby\n  cases' h with h1 h2\n  -- h1 : x \u2264 y\n  -- h2 : x \u2260 y\n  contrapose! h2\n  -- h2 : y \u2264 x\n  -- \u22a2 x = y\n  exact le_antisymm h1 h2\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1, h2\u27e9 h'\n  -- h1 : x \u2264 y\n  -- h2 : x \u2260 y\n  -- h' : y \u2264 x\n  -- \u22a2 False\n  exact h2 (le_antisymm h1 h')\n\n-- 8\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 \u00ac y \u2264 x :=\nfun \u27e8h1, h2\u27e9 h' \u21a6 h2 (le_antisymm h1 h')\n\n-- Lemas usados\n-- ============\n\n-- #check (le_antisymm : x \u2264 y \u2192 y \u2264 x \u2192 x = y)\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