{"id":8065,"date":"2024-01-06T08:58:33","date_gmt":"2024-01-06T07:58:33","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8065"},"modified":"2024-01-06T08:58:33","modified_gmt":"2024-01-06T07:58:33","slug":"06-ene-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/06-ene-24\/","title":{"rendered":"La semana en Calculemus (6 de enero de 2024)"},"content":{"rendered":"\n<p>Esta semana he publicado en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/\">Calculemus<\/a> las demostraciones con Lean4 de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. f: \u211d \u2192 \u211d no es mon\u00f3tona syss (\u2203x,y)(x \u2264 y \u2227 f(x) > f(y))<\/a><\/li>\n<li><a href=\"#ej2\">2. La funci\u00f3n x \u21a6 -x no es mon\u00f3tona creciente<\/a><\/li>\n<li><a href=\"#ej3\">3. En los \u00f3rdenes parciales, a &lt; b \u2194 a \u2264 b \u2227 a \u2260 b<\/a><\/li>\n<li><a href=\"#ej4\">4. Si \u2264 es un preorden, entonces &lt; es irreflexiva<\/a><\/li>\n<li><a href=\"#ej5\">5. Si \u2264 es un preorden, entonces &lt; es transitiva<\/a><\/li>\n<\/ul>\n<p>A continuaci\u00f3n se muestran las soluciones.<br \/>\n<!--more--><br \/>\n<a name=\"ej1\"><\/a><\/p>\n<h3>1. f: \u211d \u2192 \u211d no es mon\u00f3tona syss (\u2203x,y)[x \u2264 y \u2227 f(x) > f(y)]<\/h3>\n<p>Demostrar con Lean4 que &#92;(f: \u211d \u2192 \u211d&#92;) no es mon\u00f3tona syss &#92;((\u2203x,y)[x \u2264 y \u2227 f(x) > f(y)]&#92;)\u200b.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {f : \u211d \u2192 \u211d}\n\nexample :\n  \u00acMonotone f \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y :=\nsorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Por la siguiente cadena de equivalencias:<br \/>\n&#92;begin{align}<br \/>\n   f &#92;text{ es no mon\u00f3tona } &amp; \u2194 \u00ac(\u2200 x, y)[x \u2264 y \u2192 f(x) \u2264 f(y)] &#92;&#92;<br \/>\n                             &amp; \u2194 (\u2203 x, y)[x \u2264 y \u2227 f(x) > f(y)]<br \/>\n&#92;end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {f : \u211d \u2192 \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  \u00acMonotone f \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y :=\ncalc\n  \u00acMonotone f\n    \u2194 \u00ac\u2200 x y, x \u2264 y \u2192 f x \u2264 f y := by rw [Monotone]\n  _ \u2194 \u2203 x y, x \u2264 y \u2227 f y < f x  := by simp_all only [not_forall, not_le, exists_prop]\n  _ \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y  := by rfl\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  \u00acMonotone f \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y :=\ncalc\n  \u00acMonotone f\n    \u2194 \u00ac\u2200 x y, x \u2264 y \u2192 f x \u2264 f y := by rw [Monotone]\n  _ \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y  := by aesop\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  \u00acMonotone f \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y :=\nby\n  rw [Monotone]\n  -- \u22a2 (\u00ac\u2200 \u2983a b : \u211d\u2984, a \u2264 b \u2192 f a \u2264 f b) \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y\n  push_neg\n  -- \u22a2 (Exists fun \u2983a\u2984 => Exists fun \u2983b\u2984 => a \u2264 b \u2227 f b < f a) \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y\n  rfl\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nlemma not_Monotone_iff :\n  \u00acMonotone f \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y :=\nby\n  rw [Monotone]\n  -- \u22a2 (\u00ac\u2200 \u2983a b : \u211d\u2984, a \u2264 b \u2192 f a \u2264 f b) \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y\n  aesop\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/CNS-de_no_monotona.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 37.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. La funci\u00f3n x \u21a6 -x no es mon\u00f3tona creciente<\/h3>\n<p>Demostrar con Lean4 que la funci\u00f3n &#92;(x \u21a6 -x&#92;) no es mon\u00f3tona creciente.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport src.CNS_de_no_monotona\n\nexample : \u00acMonotone fun x : \u211d \u21a6 -x :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Usando el lema del ejercicio anterior que afirma que una funci\u00f3n f no es mon\u00f3tona syss existen x e y tales que x \u2264 y y f(x) > f(y), basta demostrar que<br \/>\n&#92;[ (\u2203 x, y)[x \u2264 y \u2227 -x > -y] &#92;]<br \/>\nBasta elegir 2 y 3 ya que<br \/>\n&#92;[ 2 \u2264 3 \u2227 -2 > -3 &#92;]<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport src.CNS_de_no_monotona\n\nexample : \u00acMonotone fun x : \u211d \u21a6 -x :=\nby\n  apply not_Monotone_iff.mpr\n  -- \u22a2 \u2203 x y, x \u2264 y \u2227 -x > -y\n  use 2, 3\n  -- \u22a2 2 \u2264 3 \u2227 -2 > -3\n  norm_num\n<\/pre>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 37.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. En los \u00f3rdenes parciales, a &lt; b \u2194 a \u2264 b \u2227 a \u2260 b<\/h3>\n<p>Demostrar con Lean4 que en los \u00f3rdenes parciales,<br \/>\n&#92;[a &lt; b \u2194 a \u2264 b \u2227 a \u2260 b&#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\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><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Usaremos los siguientes lemas<br \/>\n&#92;begin{align}<br \/>\n   &amp;(\u2200 a, b)[a &lt; b \u2194 a \u2264 b \u2227 b \u2270 a] &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;(\u2200 a, b)[a \u2264 b \u2192 b \u2264 a \u2192 a = b] &#92;tag{L2}<br \/>\n&#92;end{align}<\/p>\n<p>Por el lema L1, lo que tenemos que demostrar es<br \/>\n&#92;[ a \u2264 b \u2227 b \u2270 a \u2194 a \u2264 b \u2227 a \u2260 b &#92;]<br \/>\nLo haremos demostrando las dos implicaciones.<\/p>\n<p>(\u21d2) Supongamos que &#92;(a \u2264 b&#92;) y &#92;(b \u2270 a&#92;). Tenemos que demostrar que &#92;(a \u2260 b&#92;). Lo haremos por reducci\u00f3n al absurdo. Para ello, supongamos que &#92;(a = b&#92;). Entonces, &#92;(b \u2264 a&#92;) que es una contradicicci\u00f3n con &#92;(b \u2270 a&#92;).<\/p>\n<p>(\u21d0) Supongamos que &#92;(a \u2264 b&#92;) y &#92;(a \u2260 b&#92;). Tenemos que demostrar que &#92;(b \u2270 a&#92;). Lo haremos por reducci\u00f3n al absurdo. Para ello, supongamos que &#92;(b \u2264 a&#92;). Entonces, junto con &#92;(a \u2264 b&#92;), se tiene que &#92;(a = b&#92;) que es una contradicicci\u00f3n con &#92;(a \u2260 b&#92;).<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\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<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Caracterizacion_de_menor_en_ordenes_parciales.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 37.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. Si \u2264 es un preorden, entonces &lt; es irreflexiva<\/h3>\n<p>Demostrar con Lean4 que si &#92;(\u2264&#92;) es un preorden, entonces &#92;(&lt;&#92;) es irreflexiva.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nvariable {\u03b1 : Type _} [Preorder \u03b1]\nvariable (a : \u03b1)\n\nexample : \u00aca < a :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1 la siguiente propiedad de lo pre\u00f3rdenes<br \/>\n&#92;[ (\u2200 a, b)[a &lt; b \u2194 a \u2264 b \u2227 b \u2270 a] &#92;]<br \/>\nCon dicha propiedad, lo que tenemos que demostrar se transforma en<br \/>\n&#92;[ \u00ac(a \u2264 a \u2227 a \u2270 a) &#92;]<br \/>\nPara demostrarla, supongamos que<br \/>\n&#92;[ a \u2264 a \u2227 a \u2270 a &#92;]<br \/>\nlo que es una contradicci\u00f3n.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nvariable {\u03b1 : Type _} [Preorder \u03b1]\nvariable (a : \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u00aca < a :=\nby\n  rw [lt_iff_le_not_le]\n  -- \u22a2 \u00ac(a \u2264 a \u2227 \u00aca \u2264 a)\n  rintro \u27e8h1, h2\u27e9\n  -- h1 : a \u2264 a\n  -- h2 : \u00aca \u2264 a\n  -- \u22a2 False\n  exact h2 h1\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u00aca < a :=\n  irrefl a\n\n-- Lemas usados\n-- ============\n\n-- variable (b : \u03b1)\n-- #check (lt_iff_le_not_le : a < b \u2194 a \u2264 b \u2227 \u00acb \u2264 a)\n-- #check (irrefl a : \u00aca < a)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Preorden_es_irreflexivo.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 38.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. Si \u2264 es un preorden, entonces &lt; es transitiva<\/h3>\n<p>Demostrar con Lean4 que si &#92;(\u2264&#92;) es un preorden, entonces &#92;(&lt;&#92;) es transitiva.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\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><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1 la siguiente propiedad de los pre\u00f3rdenes<br \/>\n&#92;[ (\u2200 a, b)[a &lt; b \u2194 a \u2264 b \u2227 b \u2270 a] &#92;]<br \/>\nCon dicha propiedad, lo que tenemos que demostrar se transforma en<br \/>\n&#92;[ a \u2264 b \u2227 b \u2270 a \u2192 b \u2264 c \u2227 c \u2270 b \u2192 a \u2264 c \u2227 c \u2270 a &#92;]<br \/>\nPara demostrarla, supongamos que<br \/>\n&#92;begin{align}<br \/>\n   &amp;a \u2264 b &#92;tag{(1)} &#92;&#92;<br \/>\n   &amp;b \u2270 a &#92;tag{(2)} &#92;&#92;<br \/>\n   &amp;b \u2264 c &#92;tag{(3)} &#92;&#92;<br \/>\n   &amp;c \u2270 b &#92;tag{(4)}<br \/>\n&#92;end{align}<br \/>\ny tenemos que demostrar las siguientes relaciones<br \/>\n&#92;begin{align}<br \/>\n   &amp;a \u2264 c &#92;tag{(5)} &#92;&#92;<br \/>\n   &amp;c \u2270 a &#92;tag{(6)}<br \/>\n&#92;end{align}<\/p>\n<p>La (5) se tiene aplicando la propiedad transitiva a (1) y (3).<\/p>\n<p>Para demostrar la (6), supongamos que<br \/>\n&#92;[ c \u2264 a &#92;tag{(7)} &#92;]<br \/>\nentonces, junto a la (1), por la propieda transitiva se tiene<br \/>\n&#92;[ c \u2264 b &#92;]<br \/>\nque es una contradicci\u00f3n con la (4).<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\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>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Preorden_transitiva.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 38.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. f: \u211d \u2192 \u211d no es mon\u00f3tona syss (\u2203x,y)(x \u2264 y \u2227 f(x) > f(y)) 2. La funci\u00f3n x \u21a6 -x no es mon\u00f3tona creciente 3. En los \u00f3rdenes parciales, a &lt; b \u2194 a \u2264 b \u2227 a \u2260&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[335],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8065"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=8065"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8065\/revisions"}],"predecessor-version":[{"id":8066,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8065\/revisions\/8066"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8065"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8065"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8065"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}