{"id":8206,"date":"2024-05-25T13:44:20","date_gmt":"2024-05-25T11:44:20","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8206"},"modified":"2024-05-25T13:44:20","modified_gmt":"2024-05-25T11:44:20","slug":"25-may-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/25-may-24\/","title":{"rendered":"La semana en Calculemus (25 de mayo de 2024)"},"content":{"rendered":"\n<p>Esta semana he publicado en <a href=\"https:\/\/jaalonso.github.io\/calculemus\">Calculemus<\/a> las demostraciones con Lean4 de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. Los monoides booleanos son conmutativos<\/a><\/li>\n<li><a href=\"#ej2\">2. La composici\u00f3n de una funci\u00f3n creciente y una decreciente es decreciente<\/a><\/li>\n<li><a href=\"#ej3\">3. Si una funci\u00f3n es creciente e involutiva, entonces es la identidad<\/a><\/li>\n<li><a href=\"#ej4\">4. Si <code>f(x) \u2264 f(y) \u2192 x \u2264 y<\/code>, entonces f es inyectiva<\/a><\/li>\n<li><a href=\"#ej5\">5. Los supremos de las sucesiones crecientes son sus l\u00edmites<\/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. Los monoides booleanos son conmutativos<\/h3>\n<p>Un monoide es un conjunto junto con una operaci\u00f3n binaria que es asociativa y tiene elemento neutro.<\/p>\n<p>Un monoide &#92;(M&#92;) es booleano si<br \/>\n&#92;[ (\u2200 x \u2208 M)[x\u00b7x = 1] &#92;]<br \/>\ny es conmutativo si<br \/>\n&#92;[ (\u2200 x, y \u2208 M)[x\u00b7y = y\u00b7x] &#92;]<\/p>\n<p>En Lean4, est\u00e1 definida la clase de los monoides (como <code>Monoid<\/code>) y sus propiedades caracter\u00edsticas son<\/p>\n<pre lang=\"lean\">\n   mul_assoc : (a * b) * c = a * (b * c)\n   one_mul :   1 * a = a\n   mul_one :   a * 1 = a\n<\/pre>\n<p>Demostrar con Lean4 que los monoides booleanos son conmutativos.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Basic\n\nvariable {M : Type} [Monoid M]\n\nexample\n  (h : \u2200 x : M, x * x = 1)\n  : \u2200 x y : M, x * y = y * x :=\nby sorry\n<\/pre>\n<h4>1.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Sean &#92;(a, b \u2208 M&#92;). Se verifica la siguiente cadena de igualdades<br \/>\n&#92;begin{align}<br \/>\n   a\u00b7b &amp;= (a\u00b7b)\u00b71               &amp;&amp;&#92;text{[por mul_one]} &#92;&#92;<br \/>\n       &amp;= (a\u00b7b)\u00b7(a\u00b7a)           &amp;&amp;&#92;text{[por hip\u00f3tesis, &#92;(a\u00b7a = 1&#92;)]} &#92;&#92;<br \/>\n       &amp;= ((a\u00b7b)\u00b7a)\u00b7a           &amp;&amp;&#92;text{[por mul_assoc]} &#92;&#92;<br \/>\n       &amp;= (a\u00b7(b\u00b7a))\u00b7a           &amp;&amp;&#92;text{[por mul_assoc]} &#92;&#92;<br \/>\n       &amp;= (1\u00b7(a\u00b7(b\u00b7a)))\u00b7a       &amp;&amp;&#92;text{[por one_mul]} &#92;&#92;<br \/>\n       &amp;= ((b\u00b7b)\u00b7(a\u00b7(b\u00b7a)))\u00b7a   &amp;&amp;&#92;text{[por hip\u00f3tesis, &#92;(b\u00b7b = 1&#92;)]} &#92;&#92;<br \/>\n       &amp;= (b\u00b7(b\u00b7(a\u00b7(b\u00b7a))))\u00b7a   &amp;&amp;&#92;text{[por mul_assoc]} &#92;&#92;<br \/>\n       &amp;= (b\u00b7((b\u00b7a)\u00b7(b\u00b7a)))\u00b7a   &amp;&amp;&#92;text{[por mul_assoc]} &#92;&#92;<br \/>\n       &amp;= (b\u00b71)\u00b7a               &amp;&amp;&#92;text{[por hip\u00f3tesis, &#92;((b\u00b7a)\u00b7(b\u00b7a) = 1&#92;)]} &#92;&#92;<br \/>\n       &amp;= b\u00b7a                   &amp;&amp;&#92;text{[por mul_one]}<br \/>\n&#92;end{align}<\/p>\n<h4>1.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Basic\n\nvariable {M : Type} [Monoid M]\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 x : M, x * x = 1)\n  : \u2200 x y : M, x * y = y * x :=\nby\n  intros a b\n  calc a * b\n       = (a * b) * 1\n         := (mul_one (a * b)).symm\n     _ = (a * b) * (a * a)\n         := congrArg ((a*b) * .) (h a).symm\n     _ = ((a * b) * a) * a\n         := (mul_assoc (a*b) a a).symm\n     _ = (a * (b * a)) * a\n         := congrArg (. * a) (mul_assoc a b a)\n     _ = (1 * (a * (b * a))) * a\n         := congrArg (. * a) (one_mul (a*(b*a))).symm\n     _ = ((b * b) * (a * (b * a))) * a\n         := congrArg (. * a) (congrArg (. * (a*(b*a))) (h b).symm)\n     _ = (b * (b * (a * (b * a)))) * a\n         := congrArg (. * a) (mul_assoc b b (a*(b*a)))\n     _ = (b * ((b * a) * (b * a))) * a\n         := congrArg (. * a) (congrArg (b * .) (mul_assoc b a (b*a)).symm)\n     _ = (b * 1) * a\n         := congrArg (. * a) (congrArg (b * .) (h (b*a)))\n     _ = b * a\n         := congrArg (. * a) (mul_one b)\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 x : M, x * x = 1)\n  : \u2200 x y : M, x * y = y * x :=\nby\n  intros a b\n  calc a * b\n       = (a * b) * 1                   := by simp only [mul_one]\n     _ = (a * b) * (a * a)             := by simp only [h a]\n     _ = ((a * b) * a) * a             := by simp only [mul_assoc]\n     _ = (a * (b * a)) * a             := by simp only [mul_assoc]\n     _ = (1 * (a * (b * a))) * a       := by simp only [one_mul]\n     _ = ((b * b) * (a * (b * a))) * a := by simp only [h b]\n     _ = (b * (b * (a * (b * a)))) * a := by simp only [mul_assoc]\n     _ = (b * ((b * a) * (b * a))) * a := by simp only [mul_assoc]\n     _ = (b * 1) * a                   := by simp only [h (b*a)]\n     _ = b * a                         := by simp only [mul_one]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 x : M, x * x = 1)\n  : \u2200 x y : M, x * y = y * x :=\nby\n  intros a b\n  calc a * b\n       = (a * b) * 1                   := by simp only [mul_one]\n     _ = (a * b) * (a * a)             := by simp only [h a]\n     _ = (a * (b * a)) * a             := by simp only [mul_assoc]\n     _ = (1 * (a * (b * a))) * a       := by simp only [one_mul]\n     _ = ((b * b) * (a * (b * a))) * a := by simp only [h b]\n     _ = (b * ((b * a) * (b * a))) * a := by simp only [mul_assoc]\n     _ = (b * 1) * a                   := by simp only [h (b*a)]\n     _ = b * a                         := by simp only [mul_one]\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 x : M, x * x = 1)\n  : \u2200 x y : M, x * y = y * x :=\nby\n  intros a b\n  calc a * b\n       = (a * b) * 1                   := by simp\n     _ = (a * b) * (a * a)             := by simp only [h a]\n     _ = (a * (b * a)) * a             := by simp only [mul_assoc]\n     _ = (1 * (a * (b * a))) * a       := by simp\n     _ = ((b * b) * (a * (b * a))) * a := by simp only [h b]\n     _ = (b * ((b * a) * (b * a))) * a := by simp only [mul_assoc]\n     _ = (b * 1) * a                   := by simp only [h (b*a)]\n     _ = b * a                         := by simp\n\n-- Lemas usados\n-- ============\n\n-- variable (a b c : M)\n-- #check (mul_assoc a b c : (a * b) * c = a * (b * c))\n-- #check (mul_one a : a * 1 = a)\n-- #check (one_mul a : 1 * a = a)\n<\/pre>\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\/Los_monoides_booleanos_son_conmutativos.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>1.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Los_monoides_booleanos_son_conmutativos\nimports Main\nbegin\n\ncontext monoid\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * x = 1\"\n  shows   \"\u2200 x y. x * y = y * x\"\nproof (rule allI)+\n  fix a b\n  have \"a * b = (a * b) * 1\"\n    by (simp only: right_neutral)\n  also have \"\u2026 = (a * b) * (a * a)\"\n    by (simp only: assms)\n  also have \"\u2026 = ((a * b) * a) * a\"\n    by (simp only: assoc)\n  also have \"\u2026 = (a * (b * a)) * a\"\n    by (simp only: assoc)\n  also have \"\u2026 = (1 * (a * (b * a))) * a\"\n    by (simp only: left_neutral)\n  also have \"\u2026 = ((b * b) * (a * (b * a))) * a\"\n    by (simp only: assms)\n  also have \"\u2026 = (b * (b * (a * (b * a)))) * a\"\n    by (simp only: assoc)\n  also have \"\u2026 = (b * ((b * a) * (b * a))) * a\"\n    by (simp only: assoc)\n  also have \"\u2026 = (b * 1) * a\"\n    by (simp only: assms)\n  also have \"\u2026 = b * a\"\n    by (simp only: right_neutral)\n  finally show \"a * b = b * a\"\n    by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * x = 1\"\n  shows   \"\u2200 x y. x * y = y * x\"\nproof (rule allI)+\n  fix a b\n  have \"a * b = (a * b) * 1\"                    by simp\n  also have \"\u2026 = (a * b) * (a * a)\"             by (simp add: assms)\n  also have \"\u2026 = ((a * b) * a) * a\"             by (simp add: assoc)\n  also have \"\u2026 = (a * (b * a)) * a\"             by (simp add: assoc)\n  also have \"\u2026 = (1 * (a * (b * a))) * a\"       by simp\n  also have \"\u2026 = ((b * b) * (a * (b * a))) * a\" by (simp add: assms)\n  also have \"\u2026 = (b * (b * (a * (b * a)))) * a\" by (simp add: assoc)\n  also have \"\u2026 = (b * ((b * a) * (b * a))) * a\" by (simp add: assoc)\n  also have \"\u2026 = (b * 1) * a\"                   by (simp add: assms)\n  also have \"\u2026 = b * a\"                         by simp\n  finally show \"a * b = b * a\"                  by this\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * x = 1\"\n  shows   \"\u2200 x y. x * y = y * x\"\nproof (rule allI)+\n  fix a b\n  have \"a * b = (a * b) * (a * a)\"              by (simp add: assms)\n  also have \"\u2026 = (a * (b * a)) * a\"             by (simp add: assoc)\n  also have \"\u2026 = ((b * b) * (a * (b * a))) * a\" by (simp add: assms)\n  also have \"\u2026 = (b * ((b * a) * (b * a))) * a\" by (simp add: assoc)\n  also have \"\u2026 = (b * 1) * a\"                   by (simp add: assms)\n  finally show \"a * b = b * a\"                  by simp\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * x = 1\"\n  shows   \"\u2200 x y. x * y = y * x\"\n  by (metis assms assoc right_neutral)\n\nend\n\nend\n<\/pre>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. La composici\u00f3n de una funci\u00f3n creciente y una decreciente es decreciente<\/h3>\n<p>Sea una funci\u00f3n &#92;(f&#92;) de &#92;(\u211d&#92;) en &#92;(\u211d&#92;). Se dice que &#92;(f&#92;) es <strong>creciente<\/strong> si para todo &#92;(x&#92;) e &#92;(y&#92;) tales que &#92;(x \u2264 y&#92;) se tiene que &#92;(f(x) \u2264 f(y)&#92;). Se dice que &#92;(f&#92;) es <strong>decreciente<\/strong> si para todo &#92;(x&#92;) e &#92;(y&#92;) tales que &#92;(x \u2264 y&#92;) se tiene que &#92;(f(x) \u2265 f(y)&#92;).<\/p>\n<p>Demostrar con Lean4 que si &#92;(f&#92;) es creciente y &#92;(g&#92;) es decreciente, entonces &#92;(g \u2218 f&#92;) es decreciente.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\ndef creciente (f : \u211d \u2192 \u211d) : Prop :=\n  \u2200 {x y}, x \u2264 y \u2192 f x \u2264 f y\n\ndef decreciente (f : \u211d \u2192 \u211d) : Prop :=\n  \u2200 {x y}, x \u2264 y \u2192 f x \u2265 f y\n\nexample\n  (hf : creciente f)\n  (hg : decreciente g)\n  : decreciente (g \u2218 f) :=\nby sorry\n<\/pre>\n<h4>2.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Sean &#92;(x, y \u2208 \u211d&#92;) tales que &#92;(x \u2264 y&#92;). Entonces, por ser &#92;(f&#92;) creciente,<br \/>\n&#92;[ f(x) \u2265 f(y) &#92;]<br \/>\ny, por ser g decreciente,<br \/>\n&#92;[ g(f(x)) \u2264 g(f(y)) &#92;]<br \/>\nPor tanto,<br \/>\n&#92;[ (g \u2218 f)(x) \u2264 (g \u2218 f)(y) &#92;]<\/p>\n<h4>2.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\ndef creciente (f : \u211d \u2192 \u211d) : Prop :=\n  \u2200 {x y}, x \u2264 y \u2192 f x \u2264 f y\n\ndef decreciente (f : \u211d \u2192 \u211d) : Prop :=\n  \u2200 {x y}, x \u2264 y \u2192 f x \u2265 f y\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hf : creciente f)\n  (hg : decreciente g)\n  : decreciente (g \u2218 f) :=\nby\n  intro x y h\n  -- x y : \u211d\n  -- h : x \u2264 y\n  -- \u22a2 (g \u2218 f) x \u2265 (g \u2218 f) y\n  have h1 : f x \u2264 f y := hf h\n  show (g \u2218 f) x \u2265 (g \u2218 f) y\n  exact hg h1\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hf : creciente f)\n  (hg : decreciente g)\n  : decreciente (g \u2218 f) :=\nby\n  intro x y h\n  -- x y : \u211d\n  -- h : x \u2264 y\n  -- \u22a2 (g \u2218 f) x \u2265 (g \u2218 f) y\n  show (g \u2218 f) x \u2265 (g \u2218 f) y\n  exact hg (hf h)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hf : creciente f)\n  (hg : decreciente g)\n  : decreciente (g \u2218 f) :=\nfun {_ _} h \u21a6 hg (hf h)\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hf : creciente f)\n  (hg : decreciente g)\n  : decreciente (g \u2218 f) :=\nby\n  intros x y hxy\n  calc (g \u2218 f) x\n       = g (f x)   := rfl\n     _ \u2265 g (f y)   := hg (hf hxy)\n     _ = (g \u2218 f) y := rfl\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hf : creciente f)\n  (hg : decreciente g)\n  : decreciente (g \u2218 f) :=\nby\n  unfold creciente decreciente at *\n  -- hf : \u2200 {x y : \u211d}, x \u2264 y \u2192 f x \u2264 f y\n  -- hg : \u2200 {x y : \u211d}, x \u2264 y \u2192 g x \u2265 g y\n  -- \u22a2 \u2200 {x y : \u211d}, x \u2264 y \u2192 (g \u2218 f) x \u2265 (g \u2218 f) y\n  intros x y h\n  -- x y : \u211d\n  -- h : x \u2264 y\n  -- \u22a2 (g \u2218 f) x \u2265 (g \u2218 f) y\n  unfold Function.comp\n  -- \u22a2 g (f x) \u2265 g (f y)\n  apply hg\n  -- \u22a2 f x \u2264 f y\n  apply hf\n  -- \u22a2 x \u2264 y\n  exact h\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hf : creciente f)\n  (hg : decreciente g)\n  : decreciente (g \u2218 f) :=\nby\n  intros x y h\n  -- x y : \u211d\n  -- h : x \u2264 y\n  -- \u22a2 (g \u2218 f) x \u2265 (g \u2218 f) y\n  apply hg\n  -- \u22a2 f x \u2264 f y\n  apply hf\n  -- \u22a2 x \u2264 y\n  exact h\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hf : creciente f)\n  (hg : decreciente g)\n  : decreciente (g \u2218 f) :=\nby\n  intros x y h\n  -- x y : \u211d\n  -- h : x \u2264 y\n  -- \u22a2 (g \u2218 f) x \u2265 (g \u2218 f) y\n  apply hg\n  -- \u22a2 f x \u2264 f y\n  exact hf h\n\n-- 8\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hf : creciente f)\n  (hg : decreciente g)\n  : decreciente (g \u2218 f) :=\nby\n  intros x y h\n  -- x y : \u211d\n  -- h : x \u2264 y\n  -- \u22a2 (g \u2218 f) x \u2265 (g \u2218 f) y\n  exact hg (hf h)\n\n-- 9\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hf : creciente f)\n  (hg : decreciente g)\n  : decreciente (g \u2218 f) :=\nby tauto\n<\/pre>\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\/La_composicion_de_una_funcion_creciente_y_una_decreciente_es_decreciente.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>2.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory La_composicion_de_una_funcion_creciente_y_una_decreciente_es_decreciente\nimports Main HOL.Real\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  fixes f g :: \"real \u21d2 real\"\n  assumes \"mono f\"\n          \"antimono g\"\n  shows   \"antimono (g \u2218 f)\"\nproof (rule antimonoI)\n  fix x y :: real\n  assume \"x \u2264 y\"\n  have \"(g \u2218 f) y = g (f y)\"\n    by (simp only: o_apply)\n  also have \"\u2026 \u2264 g (f x)\"\n    using assms \u2039x \u2264 y\u203a\n    by (metis antimonoE monoD)\n  also have \"\u2026 = (g \u2218 f) x\"\n    by (simp only: o_apply)\n  finally show \"(g \u2218 f) x \u2265 (g \u2218 f) y\"\n    by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  fixes f g :: \"real \u21d2 real\"\n  assumes \"mono f\"\n          \"antimono g\"\n  shows   \"antimono (g \u2218 f)\"\nproof (rule antimonoI)\n  fix x y :: real\n  assume \"x \u2264 y\"\n  have \"(g \u2218 f) y = g (f y)\"    by simp\n  also have \"\u2026 \u2264 g (f x)\"     by (meson \u2039x \u2264 y\u203a assms antimonoE monoE)\n  also have \"\u2026 = (g \u2218 f) x\"    by simp\n  finally show \"(g \u2218 f) x \u2265 (g \u2218 f) y\" .\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"mono f\"\n          \"antimono g\"\n  shows   \"antimono (g \u2218 f)\"\n  using assms(1) assms(2) monotone_on_o\n  by blast\n\nend\n<\/pre>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. Si una funci\u00f3n es creciente e involutiva, entonces es la identidad<\/h3>\n<p>Sea una funci\u00f3n &#92;(f&#92;) de &#92;(\u211d&#92;) en &#92;(\u211d&#92;).<\/p>\n<ul>\n<li>Se dice que &#92;(f&#92;) es creciente si para todo &#92;(x&#92;) e &#92;(y&#92;) tales que &#92;(x \u2264 y&#92;) se tiene que &#92;(f(x) \u2264 f(y)&#92;).<\/li>\n<li>Se dice que &#92;(f&#92;) es involutiva si para todo &#92;(x&#92;) se tiene que &#92;(f(f(x)) = x&#92;).<\/li>\n<\/ul>\n<p>En Lean4 que &#92;(f&#92;) sea creciente se representa por <code>Monotone f<\/code> y que sea involutiva por <code>Involutive f<\/code><\/p>\n<p>Demostrar con Lean4 que si &#92;(f&#92;) es creciente e involutiva, entonces &#92;(f&#92;) es la identidad.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nopen Function\n\nvariable (f : \u211d \u2192 \u211d)\n\nexample\n  (hc : Monotone f)\n  (hi : Involutive f)\n  : f = id :=\nby sorry\n<\/pre>\n<h4>3.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Tenemos que demostrar que para todo &#92;(x \u2208 \u211d&#92;), &#92;(f(x) = x&#92;). Sea &#92;(x \u2208 \u211d&#92;). Entonces, por ser &#92;(f&#92;) involutiva, se tiene que<br \/>\n&#92;[ f(f(x)) = x &#92;tag{1} &#92;]<br \/>\nAdem\u00e1s, por las propiedades del orden, se tiene que &#92;(f(x) \u2264 x&#92;) \u00f3 &#92;(x \u2264 f(x)&#92;). Demostraremos que &#92;(f(x) = x&#92;) en los dos casos.<\/p>\n<p>Caso 1: Supongamos que<br \/>\n&#92;[ f(x) \u2264 x &#92;tag{2} &#92;]<br \/>\nEntonces, por ser &#92;(f&#92;) creciente, se tiene que<br \/>\n&#92;[ f(f(x)) \u2264 f(x) &#92;tag{3} &#92;]<br \/>\nSustituyendo (1) en (3), se tiene<br \/>\n&#92;[ x \u2264 f(x) &#92;]<br \/>\nque junto con (1) da<br \/>\n&#92;[ f(x) = x &#92;]<\/p>\n<p>Caso 2: Supongamos que<br \/>\n&#92;[ x \u2264 f(x) &#92;tag{4} &#92;]<br \/>\nEntonces, por ser &#92;(f&#92;) creciente, se tiene que<br \/>\n&#92;[ f(x) \u2264 f(f(x)) &#92;tag{5} &#92;]<br \/>\nSustituyendo (1) en (5), se tiene<br \/>\n&#92;[ f(x) \u2264 x &#92;]<br \/>\nque junto con (4) da<br \/>\n&#92;[ f(x) = x &#92;]<\/p>\n<h4>3.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nopen Function\n\nvariable (f : \u211d \u2192 \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (hc : Monotone f)\n  (hi : Involutive f)\n  : f = id :=\nby\n  funext x\n  -- x : \u211d\n  -- \u22a2 f x = id x\n  have h : f (f x) = x := hi x\n  cases' (le_total (f x) x) with h1 h2\n  . -- h1 : f x \u2264 x\n    have h1a : f (f x) \u2264 f x := hc h1\n    have h1b : x \u2264 f x := by rwa [h] at h1a\n    show f x = x\n    exact antisymm h1 h1b\n  . -- h2 : x \u2264 f x\n    have h2a : f x \u2264 f (f x) := hc h2\n    have h2b : f x \u2264 x := by rwa [h] at h2a\n    show f x = x\n    exact antisymm h2b h2\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (hc : Monotone f)\n  (hi : Involutive f)\n  : f = id :=\nby\n  unfold Monotone Involutive at *\n  -- hc : \u2200 \u2983a b : \u211d\u2984, a \u2264 b \u2192 f a \u2264 f b\n  -- hi : \u2200 (x : \u211d), f (f x) = x\n  funext x\n  -- x : \u211d\n  -- \u22a2 f x = id x\n  unfold id\n  -- \u22a2 f x = x\n  cases' (le_total (f x) x) with h1 h2\n  . -- h1 : f x \u2264 x\n    apply antisymm h1\n    -- \u22a2 x \u2264 f x\n    have h3 : f (f x) \u2264 f x := by\n      apply hc\n      -- \u22a2 f x \u2264 x\n      exact h1\n    rwa [hi] at h3\n  . -- h2 : x \u2264 f x\n    apply antisymm _ h2\n    -- \u22a2 f x \u2264 x\n    have h4 : f x \u2264 f (f x) := by\n      apply hc\n      -- \u22a2 x \u2264 f x\n      exact h2\n    rwa [hi] at h4\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (hc : Monotone f)\n  (hi : Involutive f)\n  : f = id :=\nby\n  funext x\n  -- x : \u211d\n  -- \u22a2 f x = id x\n  cases' (le_total (f x) x) with h1 h2\n  . -- h1 : f x \u2264 x\n    apply antisymm h1\n    -- \u22a2 x \u2264 f x\n    have h3 : f (f x) \u2264 f x := hc h1\n    rwa [hi] at h3\n  . -- h2 : x \u2264 f x\n    apply antisymm _ h2\n    -- \u22a2 f x \u2264 x\n    have h4 : f x \u2264 f (f x) := hc h2\n    rwa [hi] at h4\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (hc : Monotone f)\n  (hi : Involutive f)\n  : f = id :=\nby\n  funext x\n  -- x : \u211d\n  -- \u22a2 f x = id x\n  cases' (le_total (f x) x) with h1 h2\n  . -- h1 : f x \u2264 x\n    apply antisymm h1\n    -- \u22a2 x \u2264 f x\n    calc x\n         = f (f x) := (hi x).symm\n       _ \u2264 f x     := hc h1\n  . -- h2 : x \u2264 f x\n    apply antisymm _ h2\n    -- \u22a2 f x \u2264 x\n    calc f x\n         \u2264 f (f x) := hc h2\n       _ = x       := hi x\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- #check (le_total a b : a \u2264 b \u2228 b \u2264 a)\n-- #check (antisymm : a \u2264 b \u2192 b \u2264 a \u2192 a = b)\n<\/pre>\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\/Una_funcion_creciente_e_involutiva_es_la_identidad.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>3.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Una_funcion_creciente_e_involutiva_es_la_identidad\nimports Main HOL.Real\nbegin\n\ndefinition involutiva :: \"(real \u21d2 real) \u21d2 bool\"\n  where \"involutiva f \u27f7 (\u2200x. f (f x) = x)\"\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  fixes f :: \"real \u21d2 real\"\n  assumes \"mono f\"\n          \"involutiva f\"\n  shows   \"f = id\"\nproof (unfold fun_eq_iff; intro allI)\n  fix x\n  have \"x \u2264 f x \u2228 f x \u2264 x\"\n    by (rule linear)\n  then have \"f x = x\"\n  proof (rule disjE)\n    assume \"x \u2264 f x\"\n    then have \"f x \u2264 f (f x)\"\n      using assms(1) by (simp only: monoD)\n    also have \"\u2026 = x\"\n      using assms(2) by (simp only: involutiva_def)\n    finally have \"f x \u2264 x\"\n      by this\n    show \"f x = x\"\n      using \u2039f x \u2264 x\u203a \u2039x \u2264 f x\u203a by (simp only: antisym)\n  next\n    assume \"f x \u2264 x\"\n    have \"x = f (f x)\"\n      using assms(2) by (simp only: involutiva_def)\n    also have \"... \u2264 f x\"\n      using \u2039f x \u2264 x\u203a assms(1) by (simp only: monoD)\n    finally have \"x \u2264 f x\"\n      by this\n    show \"f x = x\"\n      using \u2039f x \u2264 x\u203a \u2039x \u2264 f x\u203a by (simp only: monoD)\n  qed\n  then show \"f x = id x\"\n    by (simp only: id_apply)\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  fixes f :: \"real \u21d2 real\"\n  assumes \"mono f\"\n          \"involutiva f\"\n  shows   \"f = id\"\nproof\n  fix x\n  have \"x \u2264 f x \u2228 f x \u2264 x\"\n    by (rule linear)\n  then have \"f x = x\"\n  proof\n    assume \"x \u2264 f x\"\n    then have \"f x \u2264 f (f x)\"\n      using assms(1) by (simp only: monoD)\n    also have \"\u2026 = x\"\n      using assms(2) by (simp only: involutiva_def)\n    finally have \"f x \u2264 x\"\n      by this\n    show \"f x = x\"\n      using \u2039f x \u2264 x\u203a \u2039x \u2264 f x\u203a by auto\n  next\n    assume \"f x \u2264 x\"\n    have \"x = f (f x)\"\n      using assms(2) by (simp only: involutiva_def)\n    also have \"... \u2264 f x\"\n      by (simp add: \u2039f x \u2264 x\u203a assms(1) monoD)\n    finally have \"x \u2264 f x\"\n      by this\n    show \"f x = x\"\n      using \u2039f x \u2264 x\u203a \u2039x \u2264 f x\u203a by auto\n  qed\n  then show \"f x = id x\"\n    by simp\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  fixes f :: \"real \u21d2 real\"\n  assumes \"mono f\"\n          \"involutiva f\"\n  shows   \"f = id\"\nproof\n  fix x\n  have \"x \u2264 f x \u2228 f x \u2264 x\"\n    by (rule linear)\n  then have \"f x = x\"\n  proof\n    assume \"x \u2264 f x\"\n    then have \"f x \u2264 x\"\n      by (metis assms involutiva_def mono_def)\n    then show \"f x = x\"\n      using \u2039x \u2264 f x\u203a by auto\n  next\n    assume \"f x \u2264 x\"\n    then have \"x \u2264 f x\"\n      by (metis assms involutiva_def mono_def)\n    then show \"f x = x\"\n      using \u2039f x \u2264 x\u203a by auto\n  qed\n  then show \"f x = id x\"\n    by simp\nqed\n\nend\n<\/pre>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. Si <code>f(x) \u2264 f(y) \u2192 x \u2264 y<\/code>, entonces f es inyectiva<\/h3>\n<p>Demostrar con Lean4 que si &#92;(f&#92;) una funci\u00f3n de &#92;(\u211d&#92;) en &#92;(\u211d&#92;) tal que<br \/>\n&#92;[ (\u2200 x, y)[f(x) \u2264 f(y) \u2192 x \u2264 y] &#92;]<br \/>\nentonces &#92;(f&#92;) es inyectiva.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nopen Function\n\nvariable (f : \u211d \u2192 \u211d)\n\nexample\n  (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n  : Injective f :=\nby sorry\n<\/pre>\n<h4>4.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Sean &#92;(x, y \u2208 \u211d&#92;) tales que<br \/>\n&#92;[ f(x) = f(y) &#92;tag{1} &#92;]<br \/>\nTenemos que demostrar que &#92;(x = y&#92;).<\/p>\n<p>De (1), tenemos que<br \/>\n&#92;[ f(x) \u2264 f(y) &#92;]<br \/>\ny, por la hip\u00f3tesis,<br \/>\n&#92;[ x \u2264 y &#92;tag{2} &#92;]<\/p>\n<p>Tambi\u00e9n de (1), tenemos que<br \/>\n&#92;[ f(y) \u2264 f(x) &#92;]<br \/>\ny, por la hip\u00f3tesis,<br \/>\n&#92;[ y \u2264 x &#92;tag{3} &#92;]<\/p>\n<p>De (2) y (3), tenemos que<br \/>\n&#92;[ x = y &#92;]<\/p>\n<h4>4.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nopen Function\n\nvariable (f : \u211d \u2192 \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n  : Injective f :=\nby\n  intros x y hxy\n  -- x y : \u211d\n  -- hxy : f x = f y\n  -- \u22a2 x = y\n  have h1 : f x \u2264 f y := le_of_eq hxy\n  have h2 : x \u2264 y     := h h1\n  have h3 : f y \u2264 f x := ge_of_eq hxy\n  have h4 : y \u2264 x     := h h3\n  show x = y\n  exact le_antisymm h2 h4\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n  : Injective f :=\nby\n  intros x y hxy\n  -- x y : \u211d\n  -- hxy : f x = f y\n  -- \u22a2 x = y\n  have h1 : x \u2264 y     := h (le_of_eq hxy)\n  have h2 : y \u2264 x     := h (ge_of_eq hxy)\n  show x = y\n  exact le_antisymm h1 h2\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n  : Injective f :=\nby\n  intros x y hxy\n  -- x y : \u211d\n  -- hxy : f x = f y\n  -- \u22a2 x = y\n  show x = y\n  exact le_antisymm (h (le_of_eq hxy)) (h (ge_of_eq hxy))\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n  : Injective f :=\nfun _ _ hxy \u21a6 le_antisymm (h hxy.le) (h hxy.ge)\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n  : Injective f :=\nby\n  intros x y hxy\n  -- x y : \u211d\n  -- hxy : f x = f y\n  -- \u22a2 x = y\n  apply le_antisymm\n  . -- \u22a2 x \u2264 y\n    apply h\n    -- \u22a2 f x \u2264 f y\n    exact le_of_eq hxy\n  . -- \u22a2 y \u2264 x\n    apply h\n    -- \u22a2 f y \u2264 f x\n    exact ge_of_eq hxy\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n  : Injective f :=\nby\n  intros x y hxy\n  -- x y : \u211d\n  -- hxy : f x = f y\n  -- \u22a2 x = y\n  apply le_antisymm\n  . -- \u22a2 x \u2264 y\n    exact h (le_of_eq hxy)\n  . -- \u22a2 y \u2264 x\n    exact h (ge_of_eq hxy)\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- #check (ge_of_eq : a = b \u2192 a \u2265 b)\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<\/pre>\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\/Si_f(x)_leq_f(y)_to_x_leq_y,_entonces_f_es_inyectiva.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>4.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory \"Si_f(x)_leq_f(y)_to_x_leq_y,_entonces_f_es_inyectiva\"\nimports Main HOL.Real\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  fixes f :: \"real \u21d2 real\"\n  assumes \"\u2200 x y. f x \u2264 f y \u27f6 x \u2264 y\"\n  shows   \"inj f\"\nproof (rule injI)\n  fix x y\n  assume \"f x = f y\"\n  show \"x = y\"\n  proof (rule antisym)\n    show \"x \u2264 y\"\n      by (simp only: assms \u2039f x = f y\u203a)\n  next\n    show \"y \u2264 x\"\n      by (simp only: assms \u2039f x = f y\u203a)\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  fixes f :: \"real \u21d2 real\"\n  assumes \"\u2200 x y. f x \u2264 f y \u27f6 x \u2264 y\"\n  shows   \"inj f\"\nproof (rule injI)\n  fix x y\n  assume \"f x = f y\"\n  then show \"x = y\"\n    using assms\n    by (simp add: eq_iff)\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  fixes f :: \"real \u21d2 real\"\n  assumes \"\u2200 x y. f x \u2264 f y \u27f6 x \u2264 y\"\n  shows   \"inj f\"\n  by (simp add: assms injI eq_iff)\nend\n<\/pre>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. Los supremos de las sucesiones crecientes son sus l\u00edmites<\/h3>\n<p>Sea &#92;(u&#92;) una sucesi\u00f3n creciente. Demostrar con Lean4 que si &#92;(S&#92;) es un supremo de &#92;(u&#92;), entonces el l\u00edmite de &#92;(u&#92;) es &#92;(S&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (u : \u2115 \u2192 \u211d)\nvariable (S : \u211d)\n\n-- (limite u c) expresa que el l\u00edmite de u es c.\ndef limite (u : \u2115 \u2192 \u211d) (c : \u211d) :=\n  \u2200 \u03b5 > 0, \u2203 m, \u2200 n \u2265 m, |u n - c| \u2264 \u03b5\n\n-- (supremo u S) expresa que el supremo de u es S.\ndef supremo (u : \u2115 \u2192 \u211d) (S : \u211d) :=\n  (\u2200 n, u n \u2264 S) \u2227 \u2200 \u03b5 > 0, \u2203 k, u k \u2265 S - \u03b5\n\nexample\n  (hu : Monotone u)\n  (hS : supremo u S)\n  : limite u S :=\nby sorry\n<\/pre>\n<h4>5.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Sea &#92;(\u03b5 \u2208 \u211d&#92;) tal que &#92;(\u03b5 > 0&#92;). Tenemos que demostrar que<br \/>\n&#92;[ (\u2203 m \u2208 \u2115)(\u2200 n \u2208 \u2115)[n \u2265 m \u2192 |u_n &#8211; S| \u2264 \u03b5] &#92;tag{1} &#92;]<\/p>\n<p>Por ser &#92;(S&#92;) un supremo de u, existe un k \u2208 \u2115 tal que<br \/>\n&#92;[ u_k \u2265 S &#8211; \u03b5 &#92;tag{2} &#92;]<br \/>\nVamos a demostrar que &#92;(k&#92;) verifica la condici\u00f3n de (1); es decir, que si &#92;(n \u2208 \u2115&#92;) tal que &#92;(n \u2265 k&#92;), entonces<br \/>\n&#92;[ |u_n &#8211; S| \u2264 \u03b5 &#92;]<br \/>\no, equivalentemente,<br \/>\n&#92;[ -\u03b5 \u2264 u_n &#8211; S \u2264 \u03b5 &#92;]<\/p>\n<p>La primera desigualdad se tiene por la siguente cadena:<br \/>\n&#92;begin{align}<br \/>\n   -\u03b5 &amp;= (S &#8211; \u03b5) &#8211; S    &#92;&#92;<br \/>\n      &amp;\u2264 u_k &#8211; S         &amp;&amp;&#92;text{[por (2)]} &#92;&#92;<br \/>\n      &amp;\u2264 u_n &#8211; S         &amp;&amp;&#92;text{[porque &#92;(u&#92;) es creciente y &#92;(n \u2265 k&#92;)]}<br \/>\n&#92;end{align}<\/p>\n<p>La segunda desigualdad se tiene por la siguente cadena:<br \/>\n&#92;begin{align}<br \/>\n   u_n &#8211; S &amp;\u2264 S &#8211; S      &amp;&amp;&#92;text{[porque &#92;(S&#92;) es un supremo de &#92;(u&#92;)]} &#92;&#92;<br \/>\n          &amp;= 0          &#92;&#92;<br \/>\n          &amp;\u2264 \u03b5<br \/>\n&#92;end{align}<\/p>\n<h4>5.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (u : \u2115 \u2192 \u211d)\nvariable (S : \u211d)\n\n-- (limite u c) expresa que el l\u00edmite de u es c.\ndef limite (u : \u2115 \u2192 \u211d) (c : \u211d) :=\n  \u2200 \u03b5 > 0, \u2203 m, \u2200 n \u2265 m, |u n - c| \u2264 \u03b5\n\n-- (supremo u S) expresa que el supremo de u es S.\ndef supremo (u : \u2115 \u2192 \u211d) (S : \u211d) :=\n  (\u2200 n, u n \u2264 S) \u2227 \u2200 \u03b5 > 0, \u2203 k, u k \u2265 S - \u03b5\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : Monotone u)\n  (hS : supremo u S)\n  : limite u S :=\nby\n  unfold limite\n  -- \u22a2 \u2200 (\u03b5 : \u211d), \u03b5 > 0 \u2192 \u2203 m, \u2200 (n : \u2115), n \u2265 m \u2192 |u n - S| \u2264 \u03b5\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 m, \u2200 (n : \u2115), n \u2265 m \u2192 |u n - S| \u2264 \u03b5\n  unfold supremo at hS\n  -- hS : (\u2200 (n : \u2115), u n \u2264 S) \u2227 \u2200 (\u03b5 : \u211d), \u03b5 > 0 \u2192 \u2203 k, u k \u2265 S - \u03b5\n  cases' hS with hS\u2081 hS\u2082\n  -- hS\u2081 : \u2200 (n : \u2115), u n \u2264 S\n  -- hS\u2082 : \u2200 (\u03b5 : \u211d), \u03b5 > 0 \u2192 \u2203 k, u k \u2265 S - \u03b5\n  cases' hS\u2082 \u03b5 h\u03b5 with k hk\n  -- k : \u2115\n  -- hk : u k \u2265 S - \u03b5\n  use k\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 k \u2192 |u n - S| \u2264 \u03b5\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 k\n  -- \u22a2 |u n - S| \u2264 \u03b5\n  rw [abs_le]\n  -- \u22a2 -\u03b5 \u2264 u n - S \u2227 u n - S \u2264 \u03b5\n  constructor\n  . -- \u22a2 -\u03b5 \u2264 u n - S\n    unfold Monotone at hu\n    -- hu : \u2200 \u2983a b : \u2115\u2984, a \u2264 b \u2192 u a \u2264 u b\n    specialize hu hn\n    -- hu : u k \u2264 u n\n    calc -\u03b5\n         = (S - \u03b5) - S := by ring\n       _ \u2264 u k - S     := sub_le_sub_right hk S\n       _ \u2264 u n - S     := sub_le_sub_right hu S\n  . calc u n - S\n         \u2264 S - S       := sub_le_sub_right (hS\u2081 n) S\n       _ = 0           := sub_self S\n       _ \u2264 \u03b5           := le_of_lt h\u03b5\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : Monotone u)\n  (hS : supremo u S)\n  : limite u S :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 m, \u2200 (n : \u2115), n \u2265 m \u2192 |u n - S| \u2264 \u03b5\n  cases' hS with hS\u2081 hS\u2082\n  -- hS\u2081 : \u2200 (n : \u2115), u n \u2264 S\n  -- hS\u2082 : \u2200 (\u03b5 : \u211d), \u03b5 > 0 \u2192 \u2203 k, u k \u2265 S - \u03b5\n  cases' hS\u2082 \u03b5 h\u03b5 with k hk\n  -- k : \u2115\n  -- hk : u k \u2265 S - \u03b5\n  use k\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 k \u2192 |u n - S| \u2264 \u03b5\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 k\n  -- \u22a2 |u n - S| \u2264 \u03b5\n  rw [abs_le]\n  -- \u22a2 -\u03b5 \u2264 u n - S \u2227 u n - S \u2264 \u03b5\n  constructor\n  . -- \u22a2 -\u03b5 \u2264 u n - S\n    linarith [hu hn]\n  . -- \u22a2 u n - S \u2264 \u03b5\n    linarith [hS\u2081 n]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : Monotone u)\n  (hS : supremo u S)\n  : limite u S :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 m, \u2200 (n : \u2115), n \u2265 m \u2192 |u n - S| \u2264 \u03b5\n  cases' hS with hS\u2081 hS\u2082\n  -- hS\u2081 : \u2200 (n : \u2115), u n \u2264 S\n  -- hS\u2082 : \u2200 (\u03b5 : \u211d), \u03b5 > 0 \u2192 \u2203 k, u k \u2265 S - \u03b5\n  cases' hS\u2082 \u03b5 h\u03b5 with k hk\n  -- k : \u2115\n  -- hk : u k \u2265 S - \u03b5\n  use k\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 k \u2192 |u n - S| \u2264 \u03b5\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 k\n  -- \u22a2 |u n - S| \u2264 \u03b5\n  rw [abs_le]\n  -- \u22a2 -\u03b5 \u2264 u n - S \u2227 u n - S \u2264 \u03b5\n  constructor <;> linarith [hu hn, hS\u2081 n]\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- #check (abs_le : |a| \u2264 b \u2194 -b \u2264 a \u2227 a \u2264 b)\n-- #check (le_of_lt : a < b \u2192 a \u2264 b)\n-- #check (sub_le_sub_right : a \u2264 b \u2192 \u2200 (c : \u211d), a - c \u2264 b - c)\n-- #check (sub_self a : a - a = 0)\n<\/pre>\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\/Los_supremos_de_las_sucesiones_crecientes_son_sus_limites.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>5.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Los_supremos_de_las_sucesiones_crecientes_son_sus_limites\nimports Main HOL.Real\nbegin\n\n(* (limite u c) expresa que el l\u00edmite de u es c. *)\ndefinition limite :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\" where\n  \"limite u c \u27f7 (\u2200\u03b5>0. \u2203k. \u2200n\u2265k. \u00a6u n - c\u00a6 \u2264 \u03b5)\"\n\n(* (supremo u M) expresa que el supremo de u es M. *)\ndefinition supremo :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\" where\n  \"supremo u M \u27f7 ((\u2200n. u n \u2264 M) \u2227 (\u2200\u03b5>0. \u2203k. \u2200n\u2265k. u n \u2265 M - \u03b5))\"\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"mono u\"\n          \"supremo u M\"\n  shows   \"limite u M\"\nproof (unfold limite_def; intro allI impI)\n  fix \u03b5 :: real\n  assume \"0 < \u03b5\"\n  have hM : \"((\u2200n. u n \u2264 M) \u2227 (\u2200\u03b5>0. \u2203k. \u2200n\u2265k. u n \u2265 M - \u03b5))\"\n    using assms(2)\n    by (simp add: supremo_def)\n  then have \"\u2200\u03b5>0. \u2203k. \u2200n\u2265k. u n \u2265 M - \u03b5\"\n    by (rule conjunct2)\n  then have \"\u2203k. \u2200n\u2265k. u n \u2265 M - \u03b5\"\n    by (simp only: \u20390 < \u03b5\u203a)\n  then obtain n0 where \"\u2200n\u2265n0. u n \u2265 M - \u03b5\"\n    by (rule exE)\n  have \"\u2200n\u2265n0. \u00a6u n - M\u00a6 \u2264 \u03b5\"\n  proof (intro allI impI)\n    fix n\n    assume \"n \u2265 n0\"\n    show \"\u00a6u n - M\u00a6 \u2264 \u03b5\"\n    proof (rule abs_leI)\n      have \"\u2200n. u n \u2264 M\"\n        using hM by (rule conjunct1)\n      then have \"u n - M \u2264 M - M\"\n        by simp\n      also have \"\u2026 = 0\"\n        by (simp only: diff_self)\n      also have \"\u2026 \u2264 \u03b5\"\n        using \u20390 < \u03b5\u203a by (simp only: less_imp_le)\n      finally show \"u n - M \u2264 \u03b5\"\n        by this\n    next\n      have \"-\u03b5 = (M - \u03b5) - M\"\n        by simp\n      also have \"\u2026 \u2264 u n - M\"\n        using \u2039\u2200n\u2265n0. M - \u03b5 \u2264 u n\u203a \u2039n0 \u2264 n\u203a by auto\n      finally have \"-\u03b5 \u2264 u n - M\"\n        by this\n      then show \"- (u n - M) \u2264 \u03b5\"\n        by simp\n    qed\n  qed\n  then show \"\u2203k. \u2200n\u2265k. \u00a6u n - M\u00a6 \u2264 \u03b5\"\n    by (rule exI)\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"mono u\"\n          \"supremo u M\"\n  shows   \"limite u M\"\nproof (unfold limite_def; intro allI impI)\n  fix \u03b5 :: real\n  assume \"0 < \u03b5\"\n  have hM : \"((\u2200n. u n \u2264 M) \u2227 (\u2200\u03b5>0. \u2203k. \u2200n\u2265k. u n \u2265 M - \u03b5))\"\n    using assms(2)\n    by (simp add: supremo_def)\n  then have \"\u2203k. \u2200n\u2265k. u n \u2265 M - \u03b5\"\n    using \u20390 < \u03b5\u203a by presburger\n  then obtain n0 where \"\u2200n\u2265n0. u n \u2265 M - \u03b5\"\n    by (rule exE)\n  then have \"\u2200n\u2265n0. \u00a6u n - M\u00a6 \u2264 \u03b5\"\n    using hM by auto\n  then show \"\u2203k. \u2200n\u2265k. \u00a6u n - M\u00a6 \u2264 \u03b5\"\n    by (rule exI)\nqed\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. Los monoides booleanos son conmutativos 2. La composici\u00f3n de una funci\u00f3n creciente y una decreciente es decreciente 3. Si una funci\u00f3n es creciente e involutiva, entonces es la identidad 4. Si f(x) \u2264 f(y) \u2192 x \u2264 y, entonces f&#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":"default","_kad_post_title":"default","_kad_post_layout":"default","_kad_post_sidebar_id":"","_kad_post_content_style":"default","_kad_post_vertical_padding":"default","_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":[342],"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\/8206"}],"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=8206"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8206\/revisions"}],"predecessor-version":[{"id":8207,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8206\/revisions\/8207"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8206"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8206"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8206"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}