{"id":1873,"date":"2023-12-25T06:00:55","date_gmt":"2023-12-25T04:00:55","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1873"},"modified":"2023-12-24T20:50:36","modified_gmt":"2023-12-24T18:50:36","slug":"25-dic-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/25-dic-23\/","title":{"rendered":"En \u211d, x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 y \u2270 x"},"content":{"rendered":"\n

Demostrar con Lean4 que. en \(\u211d\), \(x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 y \u2270 x\).<\/p>\n

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

\nimport Mathlib.Data.Real.Basic\nvariable (x y : \u211d)\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Supongamos que
\n\begin{align}
\n   x \u2264 y \tag{1} \\
\n   x \u2260 y \tag{2}
\n\end{align}
\nEntonces, se tiene \(x \u2264 y\) (por (1)) y, para probar \(y \u2270 x\), supongamos que
\n\[ y \u2264 x \tag{3}\]
\nAplicando la propiedad antim\u00e9trica a (1) y (3), se obtiene que \(x = y\), en contradicci\u00f3n con (2).<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Data.Real.Basic\nvariable (x y : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1 : x \u2264 y, h2 : x \u2260 y\u27e9\n  constructor\n  . show x \u2264 y\n    exact h1\n  . show \u00ac y \u2264 x\n    rintro h3 : y \u2264 x\n    -- \u22a2 False\n    have h4 : x = y := le_antisymm h1 h3\n    show False\n    exact h2 h4\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1 : x \u2264 y, h2 : x \u2260 y\u27e9\n  -- \u22a2 x \u2264 y \u2227 \u00acy \u2264 x\n  constructor\n  . show x \u2264 y\n    exact h1\n  . show \u00ac y \u2264 x\n    rintro h3 : y \u2264 x\n    -- \u22a2 False\n    show False\n    exact h2 (le_antisymm h1 h3)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1 : x \u2264 y, h2 : x \u2260 y\u27e9\n  constructor\n  . show x \u2264 y\n    exact h1\n  . show \u00ac y \u2264 x\n    exact fun h3 \u21a6 h2 (le_antisymm h1 h3)\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1, h2\u27e9\n  exact \u27e8h1, fun h3 \u21a6 h2 (le_antisymm h1 h3)\u27e9\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\n  fun \u27e8h1, h2\u27e9 \u21a6 \u27e8h1, fun h3 \u21a6 h2 (le_antisymm h1 h3)\u27e9\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1 : x \u2264 y, h2 : x \u2260 y\u27e9\n  use h1\n  exact fun h3 \u21a6 h2 (le_antisymm h1 h3)\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1, h2\u27e9\n  -- h1 : x \u2264 y\n  -- h2 : x \u2260 y\n  -- \u22a2 x \u2264 y \u2227 \u00acy \u2264 x\n  use h1\n  -- \u00acy \u2264 x\n  contrapose! h2\n  -- h2 : y \u2264 x\n  -- \u22a2 x = y\n  apply le_antisymm h1 h2\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