{"id":1901,"date":"2024-01-03T06:00:23","date_gmt":"2024-01-03T04:00:23","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1901"},"modified":"2023-12-31T09:57:33","modified_gmt":"2023-12-31T07:57:33","slug":"03-ene-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/03-ene-24\/","title":{"rendered":"En los \u00f3rdenes parciales, a < b \u2194 a \u2264 b \u2227 a \u2260 b"},"content":{"rendered":"\n

Demostrar con Lean4 que en los \u00f3rdenes parciales,
\n\[a < b \u2194 a \u2264 b \u2227 a \u2260 b\]<\/p>\n

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

\nimport Mathlib.Tactic\n\nvariable {\u03b1 : Type _} [PartialOrder \u03b1]\nvariable (a b : \u03b1)\n\nexample : a < b \u2194 a \u2264 b \u2227 a \u2260 b :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Usaremos los siguientes lemas
\n\begin{align}
\n   &(\u2200 a, b)[a < b \u2194 a \u2264 b \u2227 b \u2270 a] \tag{L1} \\
\n   &(\u2200 a, b)[a \u2264 b \u2192 b \u2264 a \u2192 a = b] \tag{L2}
\n\end{align}<\/p>\n
Por el lema L1, lo que tenemos que demostrar es
\n\[ a \u2264 b \u2227 b \u2270 a \u2194 a \u2264 b \u2227 a \u2260 b \]
\nLo haremos demostrando las dos implicaciones.<\/p>\n
(\u21d2) Supongamos que \(a \u2264 b\) y \(b \u2270 a\). Tenemos que demostrar que \(a \u2260 b\). Lo haremos por reducci\u00f3n al absurdo. Para ello, supongamos que \(a = b\). Entonces, \(b \u2264 a\) que es una contradicicci\u00f3n con \(b \u2270 a\).<\/p>\n
(\u21d0) Supongamos que \(a \u2264 b\) y \(a \u2260 b\). Tenemos que demostrar que \(b \u2270 a\). Lo haremos por reducci\u00f3n al absurdo. Para ello, supongamos que \(b \u2264 a\). Entonces, junto con \(a \u2264 b\), se tiene que \(a = b\) que es una contradicicci\u00f3n con \(a \u2260 b\).<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Tactic\n\nvariable {\u03b1 : Type _} [PartialOrder \u03b1]\nvariable (a b : \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2194 a \u2264 b \u2227 a \u2260 b :=\nby\n  rw [lt_iff_le_not_le]\n  -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2194 a \u2264 b \u2227 a \u2260 b\n  constructor\n  . -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2192 a \u2264 b \u2227 a \u2260 b\n    rintro \u27e8h1 : a \u2264 b, h2 : \u00acb \u2264 a\u27e9\n    -- \u22a2 a \u2264 b \u2227 a \u2260 b\n    constructor\n    . -- \u22a2 a \u2264 b\n      exact h1\n    . -- \u22a2 a \u2260 b\n      rintro (h3 : a = b)\n      -- \u22a2 False\n      have h4: b = a := h3.symm\n      have h5: b \u2264 a := le_of_eq h4\n      show False\n      exact h2 h5\n  . -- \u22a2 a \u2264 b \u2227 a \u2260 b \u2192 a \u2264 b \u2227 \u00acb \u2264 a\n    rintro \u27e8h5 : a \u2264 b , h6 : a \u2260 b\u27e9\n    -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a\n    constructor\n    . -- \u22a2 a \u2264 b\n      exact h5\n    . -- \u22a2 \u00acb \u2264 a\n      rintro (h7 : b \u2264 a)\n      have h8 : a = b := le_antisymm h5 h7\n      show False\n      exact h6 h8\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2194 a \u2264 b \u2227 a \u2260 b :=\nby\n  rw [lt_iff_le_not_le]\n  -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2194 a \u2264 b \u2227 a \u2260 b\n  constructor\n  . -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2192 a \u2264 b \u2227 a \u2260 b\n    rintro \u27e8h1 : a \u2264 b, h2 : \u00acb \u2264 a\u27e9\n    -- \u22a2 a \u2264 b \u2227 a \u2260 b\n    constructor\n    . -- \u22a2 a \u2264 b\n      exact h1\n    . -- \u22a2 a \u2260 b\n      rintro (h3 : a = b)\n      -- \u22a2 False\n      exact h2 (le_of_eq h3.symm)\n  . -- \u22a2 a \u2264 b \u2227 a \u2260 b \u2192 a \u2264 b \u2227 \u00acb \u2264 a\n    rintro \u27e8h4 : a \u2264 b , h5 : a \u2260 b\u27e9\n    -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a\n    constructor\n    . -- \u22a2 a \u2264 b\n      exact h4\n    . -- \u22a2 \u00acb \u2264 a\n      rintro (h6 : b \u2264 a)\n      exact h5 (le_antisymm h4 h6)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2194 a \u2264 b \u2227 a \u2260 b :=\nby\n  rw [lt_iff_le_not_le]\n  -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2194 a \u2264 b \u2227 a \u2260 b\n  constructor\n  . -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2192 a \u2264 b \u2227 a \u2260 b\n    rintro \u27e8h1 : a \u2264 b, h2 : \u00acb \u2264 a\u27e9\n    -- \u22a2 a \u2264 b \u2227 a \u2260 b\n    constructor\n    . -- \u22a2 a \u2264 b\n      exact h1\n    . -- \u22a2 a \u2260 b\n      exact fun h3 \u21a6 h2 (le_of_eq h3.symm)\n  . -- \u22a2 a \u2264 b \u2227 a \u2260 b \u2192 a \u2264 b \u2227 \u00acb \u2264 a\n    rintro \u27e8h4 : a \u2264 b , h5 : a \u2260 b\u27e9\n    -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a\n    constructor\n    . -- \u22a2 a \u2264 b\n      exact h4\n    . -- \u22a2 \u00acb \u2264 a\n      exact fun h6 \u21a6 h5 (le_antisymm h4 h6)\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2194 a \u2264 b \u2227 a \u2260 b :=\nby\n  rw [lt_iff_le_not_le]\n  -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2194 a \u2264 b \u2227 a \u2260 b\n  constructor\n  . -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2192 a \u2264 b \u2227 a \u2260 b\n    rintro \u27e8h1 : a \u2264 b, h2 : \u00acb \u2264 a\u27e9\n    -- \u22a2 a \u2264 b \u2227 a \u2260 b\n    exact \u27e8h1, fun h3 \u21a6 h2 (le_of_eq h3.symm)\u27e9\n  . -- \u22a2 a \u2264 b \u2227 a \u2260 b \u2192 a \u2264 b \u2227 \u00acb \u2264 a\n    rintro \u27e8h4 : a \u2264 b , h5 : a \u2260 b\u27e9\n    -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a\n    exact \u27e8h4, fun h6 \u21a6 h5 (le_antisymm h4 h6)\u27e9\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2194 a \u2264 b \u2227 a \u2260 b :=\nby\n  rw [lt_iff_le_not_le]\n  -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2194 a \u2264 b \u2227 a \u2260 b\n  constructor\n  . -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2192 a \u2264 b \u2227 a \u2260 b\n    exact fun \u27e8h1, h2\u27e9 \u21a6 \u27e8h1, fun h3 \u21a6 h2 (le_of_eq h3.symm)\u27e9\n  . -- \u22a2 a \u2264 b \u2227 a \u2260 b \u2192 a \u2264 b \u2227 \u00acb \u2264 a\n    exact fun \u27e8h4, h5\u27e9 \u21a6 \u27e8h4, fun h6 \u21a6 h5 (le_antisymm h4 h6)\u27e9\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2194 a \u2264 b \u2227 a \u2260 b :=\nby\n  rw [lt_iff_le_not_le]\n  -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2194 a \u2264 b \u2227 a \u2260 b\n  exact \u27e8fun \u27e8h1, h2\u27e9 \u21a6 \u27e8h1, fun h3 \u21a6 h2 (le_of_eq h3.symm)\u27e9,\n         fun \u27e8h4, h5\u27e9 \u21a6 \u27e8h4, fun h6 \u21a6 h5 (le_antisymm h4 h6)\u27e9\u27e9\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2194 a \u2264 b \u2227 a \u2260 b :=\nby\n  constructor\n  . -- \u22a2 a < b \u2192 a \u2264 b \u2227 a \u2260 b\n    intro h\n    -- h : a < b\n    -- \u22a2 a \u2264 b \u2227 a \u2260 b\n    constructor\n    . -- \u22a2 a \u2264 b\n      exact le_of_lt h\n    . -- \u22a2 a \u2260 b\n      exact ne_of_lt h\n  . -- \u22a2 a \u2264 b \u2227 a \u2260 b \u2192 a < b\n    rintro \u27e8h1, h2\u27e9\n    -- h1 : a \u2264 b\n    -- h2 : a \u2260 b\n    -- \u22a2 a < b\n    exact lt_of_le_of_ne h1 h2\n\n-- 8\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2194 a \u2264 b \u2227 a \u2260 b :=\n  \u27e8fun h \u21a6 \u27e8le_of_lt h, ne_of_lt h\u27e9,\n   fun \u27e8h1, h2\u27e9 \u21a6 lt_of_le_of_ne h1 h2\u27e9\n\n-- 9\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2194 a \u2264 b \u2227 a \u2260 b :=\n  lt_iff_le_and_ne\n\n-- Lemas usados\n-- ============\n\n-- #check (le_antisymm : a \u2264 b \u2192 b \u2264 a \u2192 a = b)\n-- #check (le_of_eq : a = b \u2192 a \u2264 b)\n-- #check (lt_iff_le_and_ne : a < b \u2194 a \u2264 b \u2227 a \u2260 b)\n-- #check (lt_iff_le_not_le : a < b \u2194 a \u2264 b \u2227 \u00acb \u2264 a)\n-- #check (lt_of_le_of_ne : a \u2264 b \u2192 a \u2260 b \u2192 a < b)\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