Demostrar con Lean4 que si \(\u2264\) es un preorden, entonces \(<\) es transitiva.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Tactic\nvariable {\u03b1 : Type _} [Preorder \u03b1]\nvariable (a b c : \u03b1)\n\nexample : a < b \u2192 b < c \u2192 a < c :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Se usar\u00e1 la siguiente propiedad de los pre\u00f3rdenes
\n\[ (\u2200 a, b)[a < b \u2194 a \u2264 b \u2227 b \u2270 a] \]
\nCon dicha propiedad, lo que tenemos que demostrar se transforma en
\n\[ a \u2264 b \u2227 b \u2270 a \u2192 b \u2264 c \u2227 c \u2270 b \u2192 a \u2264 c \u2227 c \u2270 a \]
\nPara demostrarla, supongamos que
\n\begin{align}
\n &a \u2264 b \tag{(1)} \\
\n &b \u2270 a \tag{(2)} \\
\n &b \u2264 c \tag{(3)} \\
\n &c \u2270 b \tag{(4)}
\n\end{align}
\ny tenemos que demostrar las siguientes relaciones
\n\begin{align}
\n &a \u2264 c \tag{(5)} \\
\n &c \u2270 a \tag{(6)}
\n\end{align}<\/p>\n
La (5) se tiene aplicando la propiedad transitiva a (1) y (3).<\/p>\n
Para demostrar la (6), supongamos que
\n\[ c \u2264 a \tag{(7)} \]
\nentonces, junto a la (1), por la propieda transitiva se tiene
\n\[ c \u2264 b \]
\nque es una contradicci\u00f3n con la (4).<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Tactic\nvariable {\u03b1 : Type _} [Preorder \u03b1]\nvariable (a b c : \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2192 b < c \u2192 a < c :=\nby\n simp only [lt_iff_le_not_le]\n -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2192 b \u2264 c \u2227 \u00acc \u2264 b \u2192 a \u2264 c \u2227 \u00acc \u2264 a\n rintro \u27e8h1 : a \u2264 b, _h2 : \u00acb \u2264 a\u27e9 \u27e8h3 : b \u2264 c, h4 : \u00acc \u2264 b\u27e9\n -- \u22a2 a \u2264 c \u2227 \u00acc \u2264 a\n constructor\n . -- \u22a2 a \u2264 c\n exact le_trans h1 h3\n . -- \u22a2 \u00acc \u2264 a\n contrapose! h4\n -- h4 : c \u2264 a\n -- \u22a2 c \u2264 b\n exact le_trans h4 h1\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2192 b < c \u2192 a < c :=\nby\n simp only [lt_iff_le_not_le]\n -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2192 b \u2264 c \u2227 \u00acc \u2264 b \u2192 a \u2264 c \u2227 \u00acc \u2264 a\n rintro \u27e8h1 : a \u2264 b, _h2 : \u00acb \u2264 a\u27e9 \u27e8h3 : b \u2264 c, h4 : \u00acc \u2264 b\u27e9\n -- \u22a2 a \u2264 c \u2227 \u00acc \u2264 a\n constructor\n . -- \u22a2 a \u2264 c\n exact le_trans h1 h3\n . -- \u22a2 \u00acc \u2264 a\n rintro (h5 : c \u2264 a)\n -- \u22a2 False\n have h6 : c \u2264 b := le_trans h5 h1\n show False\n exact h4 h6\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2192 b < c \u2192 a < c :=\nby\n simp only [lt_iff_le_not_le]\n -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2192 b \u2264 c \u2227 \u00acc \u2264 b \u2192 a \u2264 c \u2227 \u00acc \u2264 a\n rintro \u27e8h1 : a \u2264 b, _h2 : \u00acb \u2264 a\u27e9 \u27e8h3 : b \u2264 c, h4 : \u00acc \u2264 b\u27e9\n -- \u22a2 a \u2264 c \u2227 \u00acc \u2264 a\n constructor\n . -- \u22a2 a \u2264 c\n exact le_trans h1 h3\n . -- \u22a2 \u00acc \u2264 a\n exact fun h5 \u21a6 h4 (le_trans h5 h1)\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2192 b < c \u2192 a < c :=\nby\n simp only [lt_iff_le_not_le]\n -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2192 b \u2264 c \u2227 \u00acc \u2264 b \u2192 a \u2264 c \u2227 \u00acc \u2264 a\n rintro \u27e8h1 : a \u2264 b, _h2 : \u00acb \u2264 a\u27e9 \u27e8h3 : b \u2264 c, h4 : \u00acc \u2264 b\u27e9\n -- \u22a2 a \u2264 c \u2227 \u00acc \u2264 a\n exact \u27e8le_trans h1 h3, fun h5 \u21a6 h4 (le_trans h5 h1)\u27e9\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2192 b < c \u2192 a < c :=\nby\n simp only [lt_iff_le_not_le]\n -- \u22a2 a \u2264 b \u2227 \u00acb \u2264 a \u2192 b \u2264 c \u2227 \u00acc \u2264 b \u2192 a \u2264 c \u2227 \u00acc \u2264 a\n exact fun \u27e8h1, _h2\u27e9 \u27e8h3, h4\u27e9 \u21a6 \u27e8le_trans h1 h3,\n fun h5 \u21a6 h4 (le_trans h5 h1)\u27e9\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a < b \u2192 b < c \u2192 a < c :=\n lt_trans\n\n-- Lemas usados\n-- ============\n\n-- #check (lt_iff_le_not_le : a < b \u2194 a \u2264 b \u2227 \u00acb \u2264 a)\n-- #check (le_trans : a \u2264 b \u2192 b \u2264 c \u2192 a \u2264 c)\n-- #check (lt_trans : a < b \u2192 b < c \u2192 a < c)\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n