{"id":8144,"date":"2024-02-24T11:48:47","date_gmt":"2024-02-24T10:48:47","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8144"},"modified":"2024-02-24T11:58:05","modified_gmt":"2024-02-24T10:58:05","slug":"24-feb-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/24-feb-24\/","title":{"rendered":"La semana en Calculemus (24 de febrero de 2024)"},"content":{"rendered":"\n<p>Estas 3 \u00faltimas semanas 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. Si la sucesi\u00f3n u converge a a y la v a b, entonces u+v converge a a+b<\/a><\/li>\n<li><a href=\"#ej2\">2. Unicidad del l\u00edmite de las sucesiones convergentes<\/a><\/li>\n<li><a href=\"#ej3\">3. Si el l\u00edmite de la sucesi\u00f3n u\u2099 es a y c \u2208 \u211d, entonces el l\u00edmite de u\u2099+c es a+c<\/a><\/li>\n<li><a href=\"#ej4\">4. Si el l\u00edmite de la sucesi\u00f3n u\u2099 es a y c \u2208 \u211d, entonces el l\u00edmite de cu\u2099 es ca<\/a><\/li>\n<li><a href=\"#ej5\">5. El l\u00edmite de u\u2099 es a syss el de u\u2099-a es 0<\/a><\/li>\n<li><a href=\"#ej6\">6. Si u\u2099 y v\u2099 convergen a 0, entonces u\u2099v\u2099 converge a 0<\/a><\/li>\n<li><a href=\"#ej7\">7. Teorema del emparedado<\/a><\/li>\n<li><a href=\"#ej8\">8. Si s \u2286 t, entonces s \u2229 u \u2286 t \u2229 u<\/a><\/li>\n<li><a href=\"#ej9\">9. s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u)<\/a><\/li>\n<li><a href=\"#ej10\">10. (s \\ t) \\ u \u2286 s \\ (t \u222a u)<\/a><\/li>\n<li><a href=\"#ej11\">11. (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)<\/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. Si la sucesi\u00f3n u converge a a y la v a b, entonces u+v converge a a+b<\/h3>\n<p>Demostrar con Lean4 que si la sucesi\u00f3n &#92;(u&#92;) converge a &#92;(a&#92;) y la &#92;(v&#92;) a &#92;(b&#92;), entonces &#92;(u+v&#92;) converge a &#92;(a+b&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {s t : \u2115 \u2192 \u211d} {a b c : \u211d}\n\ndef limite (s : \u2115 \u2192 \u211d) (a : \u211d) :=\n  \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |s n - a| < \u03b5\n\nexample\n  (hu : limite u a)\n  (hv : limite v b)\n  : limite (u + v) (a + b) :=\nby sorry\n<\/pre>\n<h5>1.1. Demostraci\u00f3n en lenguaje natural<\/h5>\n<p>En la demostraci\u00f3n usaremos los siguientes lemas<br \/>\n&#92;begin{align}<br \/>\n   &amp;(\u2200 a \u2208 \u211d)&#92;left[a > 0 \u2192 &#92;frac{a}{2} > 0&#92;right]        &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;(\u2200 a, b, c \u2208 \u211d)[&#92;max(a, b) \u2264 c \u2192 a \u2264 c]    &#92;tag{L2} &#92;&#92;<br \/>\n   &amp;(\u2200 a, b, c \u2208 \u211d)[&#92;max(a, b) \u2264 c \u2192 b \u2264 c]    &#92;tag{L3} &#92;&#92;<br \/>\n   &amp;(\u2200 a, b \u2208 \u211d)[|a + b| \u2264 |a| + |b|]         &#92;tag{L4} &#92;&#92;<br \/>\n   &amp;(\u2200 a \u2208 \u211d)&#92;left[&#92;frac{a}{2} + &#92;frac{a}{2} = a&#92;right]  &#92;tag{L5}<br \/>\n&#92;end{align}<\/p>\n<p>Tenemos que probar que para todo &#92;(\u03b5 \u2208 \u211d&#92;), si<br \/>\n&#92;[ \u03b5 > 0 &#92;tag{1} &#92;]<br \/>\nentonces<br \/>\n&#92;[ (\u2203N \u2208 \u2115)(\u2200n \u2208 \u2115)[n \u2265 N \u2192 |(u + v)(n) - (a + b)| &lt; \u03b5] &#92;tag{2} &#92;]<\/p>\n<p>Por (1) y el lema L1, se tiene que<br \/>\n&#92;[ &#92;frac{\u03b5}{2} > 0 &#92;tag{3} &#92;]<br \/>\nPor (3) y porque el l\u00edmite de &#92;(u&#92;) es &#92;(a&#92;), se tiene que<br \/>\n&#92;[ (\u2203N \u2208 \u2115)(\u2200n \u2208 \u2115)&#92;left[n \u2265 N \u2192 |u(n) - a| &lt; &#92;frac{\u03b5}{2}&#92;right] &#92;]<br \/>\nSea &#92;(N\u2081 \u2208 \u2115&#92;) tal que<br \/>\n&#92;[ (\u2200n \u2208 \u2115)&#92;left[n \u2265 N\u2081 \u2192 |u(n) - a| &lt; &#92;frac{\u03b5}{2}&#92;right] &#92;tag{4} &#92;]<br \/>\nPor (3) y porque el l\u00edmite de &#92;(v&#92;) es &#92;(b&#92;), se tiene que<br \/>\n&#92;[ (\u2203N \u2208 \u2115)(\u2200n \u2208 \u2115)&#92;left[n \u2265 N \u2192 |v(n) - b| &lt; &#92;frac{\u03b5}{2}&#92;right] &#92;]<br \/>\nSea &#92;(N\u2082 \u2208 \u2115&#92;) tal que<br \/>\n&#92;[ (\u2200n \u2208 \u2115)&#92;left[n \u2265 N\u2082 \u2192 |v(n) - b| &lt; &#92;frac{\u03b5}{2}&#92;right] &#92;tag{5} &#92;]<br \/>\nSea &#92;(N = &#92;max(N\u2081, N\u2082)&#92;). Veamos que verifica la condici\u00f3n (1). Para ello, sea &#92;(n \u2208 \u2115&#92;) tal que &#92;(n \u2265 N&#92;). Entonces, &#92;(n \u2265 N\u2081&#92;) (por L2) y &#92;(n \u2265 N\u2082&#92;) (por L3). Por tanto, usando las propiedades (4) y (5) se tiene que<br \/>\n&#92;begin{align}<br \/>\n   |u(n) - a| &amp;&lt; &#92;frac{\u03b5}{2} &#92;tag{6} &#92;&#92;<br \/>\n   |v(n) - b| &amp;&lt; &#92;frac{\u03b5}{2} &#92;tag{7}<br \/>\n&#92;end{align}<br \/>\nFinalmente,<br \/>\n&#92;begin{align}<br \/>\n   |(u + v)(n) - (a + b)| &amp;= |(u(n) + v(n)) - (a + b)|    &#92;&#92;<br \/>\n                          &amp;= |(u(n) - a) + (v(n) - b)|    &#92;&#92;<br \/>\n                          &amp;\u2264 |u(n) - a| + |v(n) - b|      &amp;&amp;&#92;text{[por L4]}&#92;&#92;<br \/>\n                          &amp;&lt; &#92;frac{\u03b5}{2} + &#92;frac{\u03b5}{2}    &amp;&amp;&#92;text{[por (6) y (7)]}&#92;&#92;<br \/>\n                          &amp;= \u03b5                            &amp;&amp;&#92;text{[por L5]}<br \/>\n&#92;end{align}<\/p>\n<h5>1.2. Demostraciones con Lean4<\/h5>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {s t : \u2115 \u2192 \u211d} {a b c : \u211d}\n\ndef limite (s : \u2115 \u2192 \u211d) (a : \u211d) :=\n  \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |s n - a| < \u03b5\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : limite u a)\n  (hv : limite v b)\n  : limite (u + v) (a + b) :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(u + v) n - (a + b)| < \u03b5\n  have h\u03b52 : 0 < \u03b5 \/ 2 := half_pos h\u03b5\n  cases' hu (\u03b5 \/ 2) h\u03b52 with Nu hNu\n  -- Nu : \u2115\n  -- hNu : \u2200 (n : \u2115), n \u2265 Nu \u2192 |u n - a| < \u03b5 \/ 2\n  cases' hv (\u03b5 \/ 2) h\u03b52 with Nv hNv\n  -- Nv : \u2115\n  -- hNv : \u2200 (n : \u2115), n \u2265 Nv \u2192 |v n - b| < \u03b5 \/ 2\n  clear hu hv h\u03b52 h\u03b5\n  let N := max Nu Nv\n  use N\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 N \u2192 |(s + t) n - (a + b)| < \u03b5\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 N\n  have nNu : n \u2265 Nu := le_of_max_le_left hn\n  specialize hNu n nNu\n  -- hNu : |u n - a| < \u03b5 \/ 2\n  have nNv : n \u2265 Nv := le_of_max_le_right hn\n  specialize hNv n nNv\n  -- hNv : |v n - b| < \u03b5 \/ 2\n  clear hn nNu nNv\n  calc |(u + v) n - (a + b)|\n       = |(u n + v n) - (a + b)|  := rfl\n     _ = |(u n - a) + (v n - b)|  := by { congr; ring }\n     _ \u2264 |u n - a| + |v n - b|    := by apply abs_add\n     _ < \u03b5 \/ 2 + \u03b5 \/ 2            := by linarith [hNu, hNv]\n     _ = \u03b5                        := by apply add_halves\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : limite u a)\n  (hv : limite v b)\n  : limite (u + v) (a + b) :=\nby\n  intros \u03b5 h\u03b5\n  cases' hu (\u03b5\/2) (by linarith) with Nu hNu\n  cases' hv (\u03b5\/2) (by linarith) with Nv hNv\n  use max Nu Nv\n  intros n hn\n  have hn\u2081 : n \u2265 Nu := le_of_max_le_left hn\n  specialize hNu n hn\u2081\n  have hn\u2082 : n \u2265 Nv := le_of_max_le_right hn\n  specialize hNv n hn\u2082\n  calc |(u + v) n - (a + b)|\n       = |(u n + v n) - (a + b)|  := by rfl\n     _ = |(u n - a) + (v n -  b)| := by {congr; ring}\n     _ \u2264 |u n - a| + |v n -  b|   := by apply abs_add\n     _ < \u03b5 \/ 2 + \u03b5 \/ 2            := by linarith\n     _ = \u03b5                        := by apply add_halves\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nlemma max_ge_iff\n  {\u03b1 : Type _}\n  [LinearOrder \u03b1]\n  {p q r : \u03b1}\n  : r \u2265 max p q  \u2194 r \u2265 p \u2227 r \u2265 q :=\nmax_le_iff\n\nexample\n  (hu : limite u a)\n  (hv : limite v b)\n  : limite (u + v) (a + b) :=\nby\n  intros \u03b5 h\u03b5\n  cases' hu (\u03b5\/2) (by linarith) with Nu hNu\n  cases' hv (\u03b5\/2) (by linarith) with Nv hNv\n  use max Nu Nv\n  intros n hn\n  cases' max_ge_iff.mp hn with hn\u2081 hn\u2082\n  have cota\u2081 : |u n - a| < \u03b5\/2 := hNu n hn\u2081\n  have cota\u2082 : |v n - b| < \u03b5\/2 := hNv n hn\u2082\n  calc |(u + v) n - (a + b)|\n       = |(u n + v n) - (a + b)| := by rfl\n     _ = |(u n - a) + (v n - b)| := by { congr; ring }\n     _ \u2264 |u n - a| + |v n - b|   := by apply abs_add\n     _ < \u03b5                       := by linarith\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : limite u a)\n  (hv : limite v b)\n  : limite (u + v) (a + b) :=\nby\n  intros \u03b5 h\u03b5\n  cases' hu (\u03b5\/2) (by linarith) with Nu hNu\n  cases' hv (\u03b5\/2) (by linarith) with Nv hNv\n  use max Nu Nv\n  intros n hn\n  cases' max_ge_iff.mp hn with hn\u2081 hn\u2082\n  calc |(u + v) n - (a + b)|\n       = |u n + v n - (a + b)|   := by rfl\n     _ = |(u n - a) + (v n - b)| := by { congr; ring }\n     _ \u2264 |u n - a| + |v n - b|   := by apply abs_add\n     _ < \u03b5\/2 + \u03b5\/2               := add_lt_add (hNu n hn\u2081) (hNv n hn\u2082)\n     _ = \u03b5                       := by simp\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : limite u a)\n  (hv : limite v b)\n  : limite (u + v) (a + b) :=\nby\n  intros \u03b5 h\u03b5\n  cases' hu (\u03b5\/2) (by linarith) with Nu hNu\n  cases' hv (\u03b5\/2) (by linarith) with Nv hNv\n  use max Nu Nv\n  intros n hn\n  rw [max_ge_iff] at hn\n  calc |(u + v) n - (a + b)|\n       = |u n + v n - (a + b)|   := by rfl\n     _ = |(u n - a) + (v n - b)| := by { congr; ring }\n     _ \u2264 |u n - a| + |v n - b|   := by apply abs_add\n     _ < \u03b5                       := by linarith [hNu n (by linarith), hNv n (by linarith)]\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : limite u a)\n  (hv : limite v b)\n  : limite (u + v) (a + b) :=\nby\n  intros \u03b5 H\u03b5\n  cases' hu (\u03b5\/2) (by linarith) with L HL\n  cases' hv (\u03b5\/2) (by linarith) with M HM\n  set N := max L M with _hN\n  use N\n  have HLN : N \u2265 L := le_max_left _ _\n  have HMN : N \u2265 M := le_max_right _ _\n  intros n Hn\n  have H3 : |u n - a| < \u03b5\/2 := HL n (by linarith)\n  have H4 : |v n - b| < \u03b5\/2 := HM n (by linarith)\n  calc |(u + v) n - (a + b)|\n       = |(u n + v n) - (a + b)|   := by rfl\n     _ = |(u n - a) + (v n - b)|   := by {congr; ring }\n     _ \u2264 |(u n - a)| + |(v n - b)| := by apply abs_add\n     _ < \u03b5\/2 + \u03b5\/2                 := by linarith\n     _ = \u03b5                         := by ring\n\n-- Lemas usados\n-- ============\n\n-- variable (d : \u211d)\n-- #check (abs_add a b : |a + b| \u2264 |a| + |b|)\n-- #check (add_halves a : a \/ 2 + a \/ 2 = a)\n-- #check (add_lt_add : a < b \u2192 c < d \u2192 a + c < b + d)\n-- #check (half_pos : a > 0 \u2192 a \/ 2 > 0)\n-- #check (le_max_left a b : a \u2264 max a b)\n-- #check (le_max_right a b : b \u2264 max a b)\n-- #check (le_of_max_le_left : max a b \u2264 c \u2192 a \u2264 c)\n-- #check (le_of_max_le_right : max a b \u2264 c \u2192 b \u2264 c)\n-- #check (max_le_iff : max a b \u2264 c \u2194 a \u2264 c \u2227 b \u2264 c)\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\/Convergencia_de_la_suma.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<h5>1.3. Demostraciones con Isabelle\/HOL<\/h5>\n<pre lang=\"isar\">\ntheory Limite_de_sucesiones_constantes\nimports Main HOL.Real\nbegin\n\ndefinition limite :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\"\n  where \"limite u c \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6u n - c\u00a6 < \u03b5)\"\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma \"limite (\u03bb n. c) c\"\nproof (unfold limite_def)\n  show \"\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6c - c\u00a6 < \u03b5\"\n  proof (intro allI impI)\n    fix \u03b5 :: real\n    assume \"0 < \u03b5\"\n    have \"\u2200n\u22650::nat. \u00a6c - c\u00a6 < \u03b5\"\n    proof (intro allI impI)\n      fix n :: nat\n      assume \"0 \u2264 n\"\n      have \"c - c = 0\"\n        by (simp only: diff_self)\n      then have \"\u00a6c - c\u00a6 = 0\"\n        by (simp only: abs_eq_0_iff)\n      also have \"\u2026 < \u03b5\"\n        by (simp only: \u20390 < \u03b5\u203a)\n      finally show \"\u00a6c - c\u00a6 < \u03b5\"\n        by this\n    qed\n    then show \"\u2203k::nat. \u2200n\u2265k. \u00a6c - c\u00a6 < \u03b5\"\n      by (rule exI)\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma \"limite (\u03bb n. c) c\"\nproof (unfold limite_def)\n  show \"\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6c - c\u00a6 < \u03b5\"\n  proof (intro allI impI)\n    fix \u03b5 :: real\n    assume \"0 < \u03b5\"\n    have \"\u2200n\u22650::nat. \u00a6c - c\u00a6 < \u03b5\"          by (simp add: \u20390 < \u03b5\u203a)\n    then show \"\u2203k::nat. \u2200n\u2265k. \u00a6c - c\u00a6 < \u03b5\" by (rule exI)\n  qed\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma \"limite (\u03bb n. c) c\"\n  unfolding limite_def\n  by simp\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma \"limite (\u03bb n. c) c\"\n  by (simp add: limite_def)\n\nend\n<\/pre>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. Unicidad del l\u00edmite de las sucesiones convergentes<\/h3>\n<p>En Lean, una sucesi\u00f3n &#92;(u\u2080, u\u2081, u\u2082, ...&#92;) se puede representar mediante una funci\u00f3n &#92;((u : \u2115 \u2192 \u211d)&#92;) de forma que &#92;(u(n)&#92;) es &#92;(u\u2099&#92;).<\/p>\n<p>Se define que &#92;(a&#92;) es el l\u00edmite de la sucesi\u00f3n &#92;(u&#92;), por<\/p>\n<pre lang=\"text\">\n   def limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n     fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n<\/pre>\n<p>Demostrar con Lean4 que cada sucesi\u00f3n tiene como m\u00e1ximo un l\u00edmite.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {u : \u2115 \u2192 \u211d}\nvariable {a b : \u211d}\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n  fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n\nexample\n  (ha : limite u a)\n  (hb : limite u b)\n  : a = b :=\n  by sorry\n<\/pre>\n<h5>2.1. Demostraci\u00f3n en lenguaje natural<\/h5>\n<p>Tenemos que demostrar que si &#92;(u&#92;) es una sucesi\u00f3n y &#92;(a&#92;) y &#92;(b&#92;) son l\u00edmites de &#92;(u&#92;), entonces &#92;(a = b&#92;). Para ello, basta demostrar que &#92;(a \u2264 b&#92;) y &#92;(b \u2264 a&#92;).<\/p>\n<p>Demostraremos que &#92;(b \u2264 a&#92;) por reducci\u00f3n al absurdo. Supongamos que &#92;(b \u2270 a&#92;). Sea &#92;(\u03b5 = b - a&#92;). Entonces, \u03b5\/2 > 0 y, puesto que &#92;(a&#92;) es un l\u00edmite de &#92;(u&#92;), existe un &#92;(A \u2208 \u2115&#92;) tal que<br \/>\n&#92;[ (\u2200n \u2208 \u2115)&#92;left[n \u2265 A \u2192 |u(n) - a| &lt; &#92;frac{\u03b5}{2}&#92;right] &#92;tag{1} &#92;]<br \/>\ny, puesto que &#92;(b&#92;) tambi\u00e9n es un l\u00edmite de &#92;(u&#92;), existe un &#92;(B \u2208 \u2115&#92;) tal que<br \/>\n&#92;[ (\u2200n \u2208 \u2115)&#92;left[n \u2265 B \u2192 |u(n) - b| &lt; &#92;frac{\u03b5}{2}&#92;right] &#92;tag{2} &#92;]<br \/>\nSea &#92;(N = m\u00e1x(A, B)&#92;). Entonces, &#92;(N \u2265 A&#92;) y &#92;(N \u2265 B&#92;) y, por (2) y (3), se tiene<br \/>\n&#92;begin{align}<br \/>\n    |u(N) - a| &amp;&lt; &#92;frac{\u03b5}{2} &#92;tag{3} &#92;&#92;<br \/>\n    |u(N) - b| &amp;&lt; &#92;frac{\u03b5}{2} &#92;tag{4}<br \/>\n&#92;end{align}<br \/>\nPara obtener una contradicci\u00f3n basta probar que &#92;(\u03b5 &lt; \u03b5&#92;). Su prueba es<br \/>\n&#92;begin{align}<br \/>\n   \u03b5 &amp;= b - a                      &#92;&#92;<br \/>\n     &amp;= |b - a|                    &#92;&#92;<br \/>\n     &amp;= |(b - a) + (u(N) - u(N))|  &#92;&#92;<br \/>\n     &amp;= |(u(N) - a) + (b - u(N))|  &#92;&#92;<br \/>\n     &amp;\u2264 |u(N) - a| + |b - u(N)|    &#92;&#92;<br \/>\n     &amp;= |u(N) - a| + |u(N) - b|    &#92;&#92;<br \/>\n     &amp;&lt; &#92;frac{\u03b5}{2} + &#92;frac{\u03b5}{2}    &amp;&amp; &#92;text{[por (3) y (4)]} &#92;&#92;<br \/>\n     &amp;= \u03b5<br \/>\n&#92;end{align}<\/p>\n<p>La demostraci\u00f3n de &#92;(a \u2264 b&#92;) es an\u00e1loga a la anterior.<\/p>\n<h5>2.2. Demostraciones con Lean4<\/h5>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {u : \u2115 \u2192 \u211d}\nvariable {a b : \u211d}\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n  fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n\n-- 1\u00aa demostraci\u00f3n del lema auxiliar\n-- =================================\n\nexample\n  (ha : limite u a)\n  (hb : limite u b)\n  : b \u2264 a :=\nby\n  by_contra h\n  -- h : \u00acb \u2264 a\n  -- \u22a2 False\n  let \u03b5 := b - a\n  have h\u03b5 : \u03b5 > 0 := sub_pos.mpr (not_le.mp h)\n  have h\u03b52 : \u03b5 \/ 2 > 0 := half_pos h\u03b5\n  cases' ha (\u03b5\/2) h\u03b52 with A hA\n  -- A : \u2115\n  -- hA : \u2200 (n : \u2115), n \u2265 A \u2192 |u n - a| < \u03b5 \/ 2\n  cases' hb (\u03b5\/2) h\u03b52 with B hB\n  -- B : \u2115\n  -- hB : \u2200 (n : \u2115), n \u2265 B \u2192 |u n - b| < \u03b5 \/ 2\n  let N := max A B\n  have hAN : A \u2264 N := le_max_left A B\n  have hBN : B \u2264 N := le_max_right A B\n  specialize hA N hAN\n  -- hA : |u N - a| < \u03b5 \/ 2\n  specialize hB N hBN\n  -- hB : |u N - b| < \u03b5 \/ 2\n  have h2 : \u03b5 < \u03b5 := by calc\n    \u03b5 = b - a                   := rfl\n    _ = |b - a|                 := (abs_of_pos h\u03b5).symm\n    _ = |(b - a) + 0|           := by {congr ; exact (add_zero (b - a)).symm}\n    _ = |(b - a) + (u N - u N)| := by {congr ; exact (sub_self (u N)).symm}\n    _ = |(u N - a) + (b - u N)| := congrArg (fun x => |x|) (by ring)\n    _ \u2264 |u N - a| + |b - u N|   := abs_add (u N - a) (b - u N)\n    _ = |u N - a| + |u N - b|   := congrArg (|u N - a| + .) (abs_sub_comm b (u N))\n    _ < \u03b5 \/ 2 + \u03b5 \/ 2           := add_lt_add hA hB\n    _ = \u03b5                       := add_halves \u03b5\n  have h3 : \u00ac(\u03b5 < \u03b5) := lt_irrefl \u03b5\n  show False\n  exact h3 h2\n\n-- 2\u00aa demostraci\u00f3n del lema auxiliar\n-- =================================\n\nlemma aux\n  (ha : limite u a)\n  (hb : limite u b)\n  : b \u2264 a :=\nby\n  by_contra h\n  -- h : \u00acb \u2264 a\n  -- \u22a2 False\n  let \u03b5 := b - a\n  cases' ha (\u03b5\/2) (by linarith) with A hA\n  -- A : \u2115\n  -- hA : \u2200 (n : \u2115), n \u2265 A \u2192 |u n - a| < \u03b5 \/ 2\n  cases' hb (\u03b5\/2) (by linarith) with B hB\n  -- B : \u2115\n  -- hB : \u2200 (n : \u2115), n \u2265 B \u2192 |u n - b| < \u03b5 \/ 2\n  let N := max A B\n  have hAN : A \u2264 N := le_max_left A B\n  have hBN : B \u2264 N := le_max_right A B\n  specialize hA N hAN\n  -- hA : |u N - a| < \u03b5 \/ 2\n  specialize hB N hBN\n  -- hB : |u N - b| < \u03b5 \/ 2\n  rw [abs_lt] at hA hB\n  -- hA : -(\u03b5 \/ 2) < u N - a \u2227 u N - a < \u03b5 \/ 2\n  -- hB : -(\u03b5 \/ 2) < u N - b \u2227 u N - b < \u03b5 \/ 2\n  linarith\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (ha : limite u a)\n  (hb : limite u b)\n  : a = b :=\nle_antisymm (aux hb ha) (aux ha hb)\n\n-- Lemas usados\n-- ============\n\n-- variable (c d : \u211d)\n-- #check (not_le : \u00aca \u2264 b \u2194 b < a)\n-- #check (sub_pos : 0 < a - b \u2194 b < a)\n-- #check (half_pos : a > 0 \u2192 a \/ 2 > 0)\n-- #check (le_max_left a b : a \u2264 max a b)\n-- #check (le_max_right a b : b \u2264 max a b)\n-- #check (abs_lt : |a| < b \u2194 -b < a \u2227 a < b)\n-- #check (abs_of_pos : 0 < a \u2192 |a| = a)\n-- #check (add_zero a : a + 0 = a)\n-- #check (sub_self a : a - a = 0)\n-- #check (abs_add a b : |a + b| \u2264 |a| + |b|)\n-- #check (abs_sub_comm a b : |a - b| = |b - a|)\n-- #check (add_lt_add : a < b \u2192 c < d \u2192 a + c < b + d)\n-- #check (add_halves a : a \/ 2 + a \/ 2 = a)\n-- #check (lt_irrefl a : \u00aca < a)\n-- #check (le_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\/Unicidad_del_limite_de_las_sucesiones_convergentes.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<h5>2.3. Demostraciones con Isabelle\/HOL<\/h5>\n<pre lang=\"isar\">\ntheory Unicidad_del_limite_de_las_sucesiones_convergentes\nimports Main HOL.Real\nbegin\n\ndefinition limite :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\"\n  where \"limite u c \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6u n - c\u00a6 < \u03b5)\"\n\nlemma aux :\n  assumes \"limite u a\"\n          \"limite u b\"\n  shows   \"b \u2264 a\"\nproof (rule ccontr)\n  assume \"\u00ac b \u2264 a\"\n  let ?\u03b5 = \"b - a\"\n  have \"0 < ?\u03b5\/2\"\n    using \u2039\u00ac b \u2264 a\u203a by auto\n  obtain A where hA : \"\u2200n\u2265A. \u00a6u n - a\u00a6 < ?\u03b5\/2\"\n    using assms(1) limite_def \u20390 < ?\u03b5\/2\u203a by blast\n  obtain B where hB : \"\u2200n\u2265B. \u00a6u n - b\u00a6 < ?\u03b5\/2\"\n    using assms(2) limite_def \u20390 < ?\u03b5\/2\u203a by blast\n  let ?C = \"max A B\"\n  have hCa : \"\u2200n\u2265?C. \u00a6u n - a\u00a6 < ?\u03b5\/2\"\n    using hA by simp\n  have hCb : \"\u2200n\u2265?C. \u00a6u n - b\u00a6 < ?\u03b5\/2\"\n    using hB by simp\n  have \"\u2200n\u2265?C. \u00a6a - b\u00a6 < ?\u03b5\"\n  proof (intro allI impI)\n    fix n assume \"n \u2265 ?C\"\n    have \"\u00a6a - b\u00a6 = \u00a6(a - u n) + (u n - b)\u00a6\" by simp\n    also have \"\u2026 \u2264 \u00a6u n - a\u00a6 + \u00a6u n - b\u00a6\" by simp\n    finally show \"\u00a6a - b\u00a6 < b - a\"\n      using hCa hCb \u2039n \u2265 ?C\u203a by fastforce\n  qed\n  then show False by fastforce\nqed\n\ntheorem\n  assumes \"limite u a\"\n          \"limite u b\"\n  shows   \"a = b\"\nproof (rule antisym)\n  show \"a \u2264 b\" using assms(2) assms(1) by (rule aux)\nnext\n  show \"b \u2264 a\" using assms(1) assms(2) by (rule aux)\nqed\n\nend\n<\/pre>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. Si el l\u00edmite de la sucesi\u00f3n u\u2099 es a y c \u2208 \u211d, entonces el l\u00edmite de u\u2099+c es a+c<\/h3>\n<p>Demostrar con Lean4 que si el l\u00edmite de la sucesi\u00f3n &#92;(u\u2099&#92;) es &#92;(a&#92;) y &#92;(c \u2208 \u211d&#92;), entonces el l\u00edmite de &#92;(u\u2099+c&#92;) es &#92;(a+c&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\nvariable {u : \u2115 \u2192 \u211d}\nvariable {a c : \u211d}\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n  fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n\nexample\n  (h : limite u a)\n  : limite (fun i \u21a6 u i + c) (a + c) :=\nby sorry\n<\/pre>\n<h5>3.1. Demostraci\u00f3n en lenguaje natural<\/h5>\n<p>Sea &#92;(\u03b5 \u2208 \u211d&#92;) tal que &#92;(\u03b5 > 0&#92;). Tenemos que demostrar que<br \/>\n&#92;[ (\u2203 N)(\u2200 n \u2265 N)[|(u(n) + c) - (a + c)| &lt; \u03b5] &#92;tag{1} &#92;]<br \/>\nPuesto que el l\u00edmite de la sucesi\u00f3n &#92;(u&#92;) es &#92;(a&#92;), existe un &#92;(k&#92;) tal que<br \/>\n&#92;[ (\u2200 n \u2265 k)[|u(n) - a| &lt; \u03b5] &#92;tag{2} &#92;]<br \/>\nVeamos que con k se verifica (1); es decir, que<br \/>\n&#92;[ (\u2200 n \u2265 k)[|(u(n) + c) - (a + c)| &lt; \u03b5] &#92;]<br \/>\nSea &#92;(n \u2265 k&#92;). Entonces, por (2),<br \/>\n&#92;[ |u(n) - a| &lt; \u03b5 &#92;tag{3} &#92;]<br \/>\ny, por consiguiente,<br \/>\n&#92;begin{align}<br \/>\n   |(u(n) + c) - (a + c)| &amp;= |u(n) - a|   &#92;&#92;<br \/>\n                          &amp;&lt; \u03b5            &amp;&amp;&#92;text{[por (3)]}<br \/>\n&#92;end{align}<\/p>\n<h5>3.2. Demostraciones con Lean4<\/h5>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\nvariable {u : \u2115 \u2192 \u211d}\nvariable {a c : \u211d}\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n  fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : limite u a)\n  : limite (fun i \u21a6 u i + c) (a + c) :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(fun i => u i + c) n - (a + c)| < \u03b5\n  dsimp\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |u n + c - (a + c)| < \u03b5\n  cases' h \u03b5 h\u03b5 with k hk\n  -- k : \u2115\n  -- hk : \u2200 (n : \u2115), n \u2265 k \u2192 |u n - a| < \u03b5\n  use k\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 k \u2192 |u n + c - (a + c)| < \u03b5\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 k\n  calc |u n + c - (a + c)|\n       = |u n - a|         := by norm_num\n     _ < \u03b5                 := hk n hn\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : limite u a)\n  : limite (fun i \u21a6 u i + c) (a + c) :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(fun i => u i + c) n - (a + c)| < \u03b5\n  dsimp\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |u n + c - (a + c)| < \u03b5\n  cases' h \u03b5 h\u03b5 with k hk\n  -- k : \u2115\n  -- hk : \u2200 (n : \u2115), n \u2265 k \u2192 |u n - a| < \u03b5\n  use k\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 k \u2192 |u n + c - (a + c)| < \u03b5\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 k\n  -- \u22a2 |u n + c - (a + c)| < \u03b5\n  convert hk n hn using 2\n  -- \u22a2 u n + c - (a + c) = u n - a\n  ring\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : limite u a)\n  : limite (fun i \u21a6 u i + c) (a + c) :=\nby\n  intros \u03b5 h\u03b5\n  dsimp\n  convert h \u03b5 h\u03b5 using 6\n  ring\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : limite u a)\n  : limite (fun i \u21a6 u i + c) (a + c) :=\n  fun \u03b5 h\u03b5 \u21a6 (by convert h \u03b5 h\u03b5 using 6; ring)\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\/Limite_cuando_se_suma_una_constante.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<h5>3.3. Demostraciones con Isabelle\/HOL<\/h5>\n<pre lang=\"isar\">\ntheory Limite_cuando_se_suma_una_constante\nimports Main HOL.Real\nbegin\n\ndefinition limite :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\"\n  where \"limite u c \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6u n - c\u00a6 < \u03b5)\"\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"limite u a\"\n  shows   \"limite (\u03bb i.  u i + c)  (a + c)\"\nproof (unfold limite_def)\n  show \"\u2200\u03b5>0. \u2203k. \u2200n\u2265k. \u00a6(u n + c) - (a + c)\u00a6 < \u03b5\"\n  proof (intro allI impI)\n    fix \u03b5 :: real\n    assume \"0 < \u03b5\"\n    then have \"\u2203k. \u2200n\u2265k. \u00a6u n - a\u00a6 < \u03b5\"\n      using assms limite_def by simp\n    then obtain k where \"\u2200n\u2265k. \u00a6u n - a\u00a6 < \u03b5\"\n      by (rule exE)\n    then have \"\u2200n\u2265k. \u00a6(u n + c) - (a + c)\u00a6 < \u03b5\"\n      by simp\n    then show \"\u2203k. \u2200n\u2265k. \u00a6(u n + c) - (a + c)\u00a6 < \u03b5\"\n      by (rule exI)\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"limite u a\"\n  shows   \"limite (\u03bb i.  u i + c)  (a + c)\"\n  using assms limite_def\n  by simp\n\nend\n<\/pre>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. Si el l\u00edmite de la sucesi\u00f3n u\u2099 es a y c \u2208 \u211d, entonces el l\u00edmite de cu\u2099 es ca<\/h3>\n<p>Demostrar con Lean4 que si el l\u00edmite de la sucesi\u00f3n &#92;(u\u2099&#92;) es &#92;(a&#92;) y &#92;(c \u2208 \u211d&#92;), entonces el l\u00edmite de &#92;(cu\u2099&#92;) es &#92;(ca&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable (u v : \u2115 \u2192 \u211d)\nvariable (a c : \u211d)\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n  fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n\nexample\n  (h : limite u a)\n  : limite (fun n \u21a6 c * (u n)) (c * a) :=\nby\n<\/pre>\n<h5>4.1. Demostraci\u00f3n en lenguaje natural<\/h5>\n<p>Sea &#92;(\u03b5 \u2208 \u211d&#92;) tal que &#92;(\u03b5 > 0&#92;). Tenemos que demostrar que<br \/>\n&#92;[ (\u2203 N \u2208 \u2115)(\u2200 n \u2265 N)[|cu\u2099 - ca| &lt; \u03b5] &#92;tag{1}&#92;]<br \/>\nDistinguiremos dos casos seg\u00fan sea &#92;(c = 0&#92;) o no.<\/p>\n<p>Primer caso: Supongamos que &#92;(c = 0&#92;). Entonces, (1) se reduce a<br \/>\n&#92;[ (\u2203 N \u2208 \u2115)(\u2200 n \u2265 N)[|0\u00b7u\u2099 - 0\u00b7a| &lt; \u03b5] &#92;]<br \/>\nes decir,<br \/>\n&#92;[ (\u2203 N \u2208 \u2115)(\u2200 n \u2265 N)[0 &lt; \u03b5] &#92;]<br \/>\nque se verifica para cualquier n\u00famero &#92;(N&#92;), ya que &#92;(\u03b5 > 0&#92;).<\/p>\n<p>Segundo caso: Supongamos que &#92;(c \u2260 0&#92;). Entonces, &#92;(&#92;dfrac{\u03b5}{|c|}&#92;) > 0 y, puesto que el l\u00edmite de &#92;(u\u2099&#92;) es &#92;(a&#92;), existe un &#92;(k \u2208 \u2115&#92;) tal que<br \/>\n&#92;[ (\u2200 n \u2265 k)[|u\u2099 - a| &lt; &#92;frac{\u03b5}{|c|}] &#92;tag{2} &#92;]<br \/>\nVeamos que con &#92;(k&#92;) se cumple (1). En efecto, sea &#92;(n \u2265 k&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   |cu\u2099 - ca| &amp;= |c(u\u2099 - a)|    &#92;&#92;<br \/>\n              &amp;= |c||u\u2099 - a|   &#92;&#92;<br \/>\n              &amp;&lt; |c|&#92;frac{\u03b5}{|c|}     &amp;&amp;&#92;text{[por (2)]} &#92;&#92;<br \/>\n              &amp;= \u03b5<br \/>\n&#92;end{align}<\/p>\n<h5>4.2. Demostraciones con Lean4<\/h5>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable (u v : \u2115 \u2192 \u211d)\nvariable (a c : \u211d)\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n  fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : limite u a)\n  : limite (fun n \u21a6 c * (u n)) (c * a) :=\nby\n  by_cases hc : c = 0\n  . -- hc : c = 0\n    subst hc\n    -- \u22a2 limite (fun n => 0 * u n) (0 * a)\n    intros \u03b5 h\u03b5\n    -- \u03b5 : \u211d\n    -- h\u03b5 : \u03b5 > 0\n    -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(fun n => 0 * u n) n - 0 * a| < \u03b5\n    aesop\n  . -- hc : \u00acc = 0\n    intros \u03b5 h\u03b5\n    -- \u03b5 : \u211d\n    -- h\u03b5 : \u03b5 > 0\n    -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(fun n => c * u n) n - c * a| < \u03b5\n    have hc' : 0 < |c| := abs_pos.mpr hc\n    have h\u03b5c : 0 < \u03b5 \/ |c| := div_pos h\u03b5 hc'\n    specialize h (\u03b5\/|c|) h\u03b5c\n    -- h : \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |u n - a| < \u03b5 \/ |c|\n    cases' h with N hN\n    -- N : \u2115\n    -- hN : \u2200 (n : \u2115), n \u2265 N \u2192 |u n - a| < \u03b5 \/ |c|\n    use N\n    -- \u22a2 \u2200 (n : \u2115), n \u2265 N \u2192 |(fun n => c * u n) n - c * a| < \u03b5\n    intros n hn\n    -- n : \u2115\n    -- hn : n \u2265 N\n    -- \u22a2 |(fun n => c * u n) n - c * a| < \u03b5\n    specialize hN n hn\n    -- hN : |u n - a| < \u03b5 \/ |c|\n    dsimp only\n    calc |c * u n - c * a|\n         = |c * (u n - a)| := congr_arg abs (mul_sub c (u n) a).symm\n       _ = |c| * |u n - a| := abs_mul c  (u n - a)\n       _ < |c| * (\u03b5 \/ |c|) := (mul_lt_mul_left hc').mpr hN\n       _ = \u03b5               := mul_div_cancel' \u03b5 (ne_of_gt hc')\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : limite u a)\n  : limite (fun n \u21a6 c * (u n)) (c * a) :=\nby\n  by_cases hc : c = 0\n  . -- hc : c = 0\n    subst hc\n    -- \u22a2 limite (fun n => 0 * u n) (0 * a)\n    intros \u03b5 h\u03b5\n    -- \u03b5 : \u211d\n    -- h\u03b5 : \u03b5 > 0\n    -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(fun n => 0 * u n) n - 0 * a| < \u03b5\n    aesop\n  . -- hc : \u00acc = 0\n    intros \u03b5 h\u03b5\n    -- \u03b5 : \u211d\n    -- h\u03b5 : \u03b5 > 0\n    -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(fun n => c * u n) n - c * a| < \u03b5\n    have hc' : 0 < |c| := abs_pos.mpr hc\n    have h\u03b5c : 0 < \u03b5 \/ |c| := div_pos h\u03b5 hc'\n    specialize h (\u03b5\/|c|) h\u03b5c\n    -- h : \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |u n - a| < \u03b5 \/ |c|\n    cases' h with N hN\n    -- N : \u2115\n    -- hN : \u2200 (n : \u2115), n \u2265 N \u2192 |u n - a| < \u03b5 \/ |c|\n    use N\n    -- \u22a2 \u2200 (n : \u2115), n \u2265 N \u2192 |(fun n => c * u n) n - c * a| < \u03b5\n    intros n hn\n    -- n : \u2115\n    -- hn : n \u2265 N\n    -- \u22a2 |(fun n => c * u n) n - c * a| < \u03b5\n    specialize hN n hn\n    -- hN : |u n - a| < \u03b5 \/ |c|\n    dsimp only\n    -- \u22a2 |c * u n - c * a| < \u03b5\n    rw [\u2190 mul_sub]\n    -- \u22a2 |c * (u n - a)| < \u03b5\n    rw [abs_mul]\n    -- \u22a2 |c| * |u n - a| < \u03b5\n    rw [\u2190 lt_div_iff' hc']\n    -- \u22a2 |u n - a| < \u03b5 \/ |c|\n    exact hN\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : limite u a)\n  : limite (fun n \u21a6 c * (u n)) (c * a) :=\nby\n  by_cases hc : c = 0\n  . subst hc\n    intros \u03b5 h\u03b5\n    aesop\n  . intros \u03b5 h\u03b5\n    have hc' : 0 < |c| := by aesop\n    have h\u03b5c : 0 < \u03b5 \/ |c| := div_pos h\u03b5 hc'\n    cases' h (\u03b5\/|c|) h\u03b5c with N hN\n    use N\n    intros n hn\n    specialize hN n hn\n    dsimp only\n    rw [\u2190 mul_sub, abs_mul, \u2190 lt_div_iff' hc']\n    exact hN\n\n-- Lemas usados\n-- ============\n\n-- variable (b c : \u211d)\n-- #check (abs_mul a b : |a * b| = |a| * |b|)\n-- #check (abs_pos.mpr : a \u2260 0 \u2192 0 < |a|)\n-- #check (div_pos : 0 < a \u2192 0 < b \u2192 0 < a \/ b)\n-- #check (lt_div_iff' : 0 < c \u2192 (a < b \/ c \u2194 c * a < b))\n-- #check (mul_div_cancel' a : b \u2260 0 \u2192 b * (a \/ b) = a)\n-- #check (mul_lt_mul_left : 0 < a \u2192 (a * b < a * c \u2194 b < c))\n-- #check (mul_sub a b c : a * (b - c) = a * b - a * c)\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\/Limite_multiplicado_por_una_constante.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<h5>4.3. Demostraciones con Isabelle\/HOL<\/h5>\n<pre lang=\"isar\">\ntheory Limite_multiplicado_por_una_constante\nimports Main HOL.Real\nbegin\n\ndefinition limite :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\"\n  where \"limite u c \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6u n - c\u00a6 < \u03b5)\"\n\nlemma\n  assumes \"limite u a\"\n  shows   \"limite (\u03bb n. c * u n) (c * a)\"\nproof (unfold limite_def)\n  show \"\u2200\u03b5>0. \u2203k. \u2200n\u2265k. \u00a6c * u n - c * a\u00a6 < \u03b5\"\n  proof (intro allI impI)\n    fix \u03b5 :: real\n    assume \"0 < \u03b5\"\n    show \"\u2203k. \u2200n\u2265k. \u00a6c * u n - c * a\u00a6 < \u03b5\"\n    proof (cases \"c = 0\")\n      assume \"c = 0\"\n      then show \"\u2203k. \u2200n\u2265k. \u00a6c * u n - c * a\u00a6 < \u03b5\"\n        by (simp add: \u20390 < \u03b5\u203a)\n    next\n      assume \"c \u2260 0\"\n      then have \"0 < \u00a6c\u00a6\"\n        by simp\n      then have \"0 < \u03b5\/\u00a6c\u00a6\"\n        by (simp add: \u20390 < \u03b5\u203a)\n      then obtain N where hN : \"\u2200n\u2265N. \u00a6u n - a\u00a6 < \u03b5\/\u00a6c\u00a6\"\n        using assms limite_def\n        by auto\n      have \"\u2200n\u2265N. \u00a6c * u n - c * a\u00a6 < \u03b5\"\n      proof (intro allI impI)\n        fix n\n        assume \"n \u2265 N\"\n        have \"\u00a6c * u n - c * a\u00a6 = \u00a6c * (u n - a)\u00a6\"\n          by argo\n        also have \"\u2026 = \u00a6c\u00a6 * \u00a6u n - a\u00a6\"\n          by (simp only: abs_mult)\n        also have \"\u2026 < \u00a6c\u00a6 * (\u03b5\/\u00a6c\u00a6)\"\n          using hN \u2039n \u2265 N\u203a \u20390 < \u00a6c\u00a6\u203a\n          by (simp only: mult_strict_left_mono)\n        finally show \"\u00a6c * u n - c * a\u00a6 < \u03b5\"\n          using \u20390 < \u00a6c\u00a6\u203a\n          by auto\n      qed\n      then show \"\u2203k. \u2200n\u2265k. \u00a6c * u n - c * a\u00a6 < \u03b5\"\n        by (rule exI)\n    qed\n  qed\nqed\n\nend\n<\/pre>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. El l\u00edmite de u\u2099 es a syss el de u\u2099-a es 0<\/h3>\n<p>Demostrar con Lean4 que el l\u00edmite de &#92;(u\u2099&#92;) es &#92;(a&#92;) si, y s\u00f3lo si, el de &#92;(u\u2099-a&#92;) es &#92;(0&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable  {u : \u2115 \u2192 \u211d}\nvariable {a c x : \u211d}\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n\nexample\n  : limite u a \u2194 limite (fun i \u21a6 u i - a) 0 :=\nby sorry\n<\/pre>\n<h5>5.1. Demostraci\u00f3n en lenguaje natural<\/h5>\n<p>Se prueba por la siguiente cadena de equivalencias<br \/>\n&#92;begin{align}<br \/>\n   &amp;&#92;text{el l\u00edmite de &#92;(u\u2099&#92;) es &#92;(a&#92;)} &#92;&#92;<br \/>\n   &amp;\u2194 (\u2200\u03b5>0)(\u2203N)(\u2200n\u2265N)[|u(n) - a| &lt; \u03b5] &#92;&#92;<br \/>\n   &amp;\u2194 (\u2200\u03b5>0)(\u2203N)(\u2200n\u2265N)[|(u(n) - a) - 0| &lt; \u03b5] &#92;&#92;<br \/>\n   &amp;\u2194 &#92;text{el l\u00edmite de &#92;(u\u2099-a&#92;) es &#92;(0&#92;)}<br \/>\n&#92;end{align}<\/p>\n<h5>5.2. Demostraciones con Lean4<\/h5>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable  {u : \u2115 \u2192 \u211d}\nvariable {a c x : \u211d}\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  : limite u a \u2194 limite (fun i \u21a6 u i - a) 0 :=\nby\n  rw [iff_eq_eq]\n  calc limite u a\n       = \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - a| < \u03b5       := rfl\n     _ = \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |(u n - a) - 0| < \u03b5 := by simp\n     _ = limite (fun i \u21a6 u i - a) 0                 := rfl\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  : limite u a \u2194 limite (fun i \u21a6 u i - a) 0 :=\nby\n  constructor\n  . -- \u22a2 limite u a \u2192 limite (fun i => u i - a) 0\n    intros h \u03b5 h\u03b5\n    -- h : limite u a\n    -- \u03b5 : \u211d\n    -- h\u03b5 : \u03b5 > 0\n    -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(fun i => u i - a) n - 0| < \u03b5\n    convert h \u03b5 h\u03b5 using 2\n    -- x : \u2115\n    -- \u22a2 (\u2200 (n : \u2115), n \u2265 x \u2192 |(fun i => u i - a) n - 0| < \u03b5) \u2194 \u2200 (n : \u2115), n \u2265 x \u2192 |u n - a| < \u03b5\n    norm_num\n  . -- \u22a2 limite (fun i => u i - a) 0 \u2192 limite u a\n    intros h \u03b5 h\u03b5\n    -- h : limite (fun i => u i - a) 0\n    -- \u03b5 : \u211d\n    -- h\u03b5 : \u03b5 > 0\n    -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |u n - a| < \u03b5\n    convert h \u03b5 h\u03b5 using 2\n    -- x : \u2115\n    -- \u22a2 (\u2200 (n : \u2115), n \u2265 x \u2192 |u n - a| < \u03b5) \u2194 \u2200 (n : \u2115), n \u2265 x \u2192 |(fun i => u i - a) n - 0| < \u03b5\n    norm_num\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  : limite u a \u2194 limite (fun i \u21a6 u i - a) 0 :=\nby\n  constructor <;>\n  { intros h \u03b5 h\u03b5\n    convert h \u03b5 h\u03b5 using 2\n    norm_num }\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nlemma limite_con_suma\n  (c : \u211d)\n  (h : limite u a)\n  : limite (fun i \u21a6 u i + c) (a + c) :=\n  fun \u03b5 h\u03b5 \u21a6 (by convert h \u03b5 h\u03b5 using 2; norm_num)\n\nlemma CNS_limite_con_suma\n  (c : \u211d)\n  : limite u a \u2194 limite (fun i \u21a6 u i + c) (a + c) :=\nby\n  constructor\n  . -- \u22a2 limite u a \u2192 limite (fun i => u i + c) (a + c)\n    apply limite_con_suma\n  . -- \u22a2 limite (fun i => u i + c) (a + c) \u2192 limite u a\n    intro h\n    -- h : limite (fun i => u i + c) (a + c)\n    -- \u22a2 limite u a\n    convert limite_con_suma (-c) h using 2\n    . -- \u22a2 u x = u x + c + -c\n      simp\n    . -- \u22a2 a = a + c + -c\n      simp\n\nexample\n  (u : \u2115 \u2192 \u211d)\n  (a : \u211d)\n  : limite u a \u2194 limite (fun i \u21a6 u i - a) 0 :=\nby\n  convert CNS_limite_con_suma (-a) using 2\n  -- \u22a2 0 = a + -a\n  simp\n\n-- Lemas usados\n-- ============\n\n-- variable (p q : Prop)\n-- #check (iff_eq_eq : (p \u2194 q) = (p = q))\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\/El_limite_de_u_es_a_syss_el_de_u-a_es_0.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<h5>5.3. Demostraciones con Isabelle\/HOL<\/h5>\n<pre lang=\"isar\">\ntheory \"El_limite_de_u_es_a_syss_el_de_u-a_es_0\"\nimports Main HOL.Real\nbegin\n\ndefinition limite :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\"\n  where \"limite u c \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6u n - c\u00a6 < \u03b5)\"\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  \"limite u a \u27f7 limite (\u03bb i. u i - a) 0\"\nproof -\n  have \"limite u a \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6u n - a\u00a6 < \u03b5)\"\n    by (rule limite_def)\n  also have \"\u2026 \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6(u n - a) - 0\u00a6 < \u03b5)\"\n    by simp\n  also have \"\u2026 \u27f7 limite (\u03bb i. u i - a) 0\"\n    by (rule limite_def[symmetric])\n  finally show \"limite u a \u27f7 limite (\u03bb i. u i - a) 0\"\n    by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  \"limite u a \u27f7 limite (\u03bb i. u i - a) 0\"\nproof -\n  have \"limite u a \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6u n - a\u00a6 < \u03b5)\"\n    by (simp only: limite_def)\n  also have \"\u2026 \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6(u n - a) - 0\u00a6 < \u03b5)\"\n    by simp\n  also have \"\u2026 \u27f7 limite (\u03bb i. u i - a) 0\"\n    by (simp only: limite_def)\n  finally show \"limite u a \u27f7 limite (\u03bb i. u i - a) 0\"\n    by this\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  \"limite u a \u27f7 limite (\u03bb i. u i - a) 0\"\n  using limite_def\n  by simp\n\nend\n<\/pre>\n<p><a name=\"ej6\"><\/a><\/p>\n<h3>6. Si u\u2099 y v\u2099 convergen a 0, entonces u\u2099v\u2099 converge a 0<\/h3>\n<p>Demostrar con Lean4 que si &#92;(u\u2099&#92;) y &#92;(v\u2099&#92;) convergen a &#92;(0&#92;), entonces &#92;(u\u2099v\u2099&#92;) converge a &#92;(0).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable {u v : \u2115 \u2192 \u211d}\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n  fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n\nexample\n  (hu : limite u 0)\n  (hv : limite v 0)\n  : limite (u * v) 0 :=\nby sorry\n<\/pre>\n<h5>6.1. Demostraci\u00f3n en lenguaje natural<\/h5>\n<p>Sea &#92;(\u03b5 \u2208 \u211d&#92;) tal que &#92;(\u03b5 > 0&#92;). Tenemos que demostrar que<br \/>\n&#92;[ (\u2203N \u2208 \u2115)(\u2200n \u2265 N)[|(u\u00b7v)(n) - 0| &lt; \u03b5] &#92;tag{1} &#92;]<br \/>\nPuesto que el l\u00edmite de &#92;(u\u2099&#92;) es &#92;(0&#92;), existe un &#92;(U \u2208 \u2115&#92;) tal que<br \/>\n&#92;[ (\u2200n \u2265 U)[|u(n) - 0| &lt; \u03b5] &#92;tag{2} &#92;]<br \/>\ny, puesto que el l\u00edmite de &#92;(v\u2099&#92;) es &#92;(0&#92;), existe un &#92;(V \u2208 \u2115&#92;) tal que<br \/>\n&#92;[ (\u2200n \u2265 V)[|v(n) - 0| &lt; 1] &#92;tag{3} &#92;]<br \/>\nEntonces, &#92;(N = &#92;text{m\u00e1x}(U, V)&#92;) cumple (1). En efecto, sea &#92;(n \u2265 N&#92;). Entonces,<br \/>\n&#92;(n \u2265 U&#92;) y &#92;(n \u2265 V&#92;) y, aplicando (2) y (3), se tiene<br \/>\n&#92;begin{align}<br \/>\n   &amp;|u(n) - 0| &lt; \u03b5 &#92;tag{4} &#92;&#92;<br \/>\n   &amp;|v(n) - 0| &lt; 1 &#92;tag{5}<br \/>\n&#92;end{align}<br \/>\nPor tanto,<br \/>\n&#92;begin{align}<br \/>\n   |(u\u00b7v)(n) - 0| &amp;= |u(n)\u00b7v(n)|     &#92;&#92;<br \/>\n                  &amp;= |u(n)|\u00b7|v n|    &#92;&#92;<br \/>\n                  &amp;&lt; \u03b5\u00b71             &amp;&amp;&#92;text{[por (4) y (5)]} &#92;&#92;<br \/>\n                  &amp;= \u03b5<br \/>\n&#92;end{align}<\/p>\n<h5>6.2. Demostraciones con Lean4<\/h5>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable {u v : \u2115 \u2192 \u211d}\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n  fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : limite u 0)\n  (hv : limite v 0)\n  : limite (u * v) 0 :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(u * v) n - 0| < \u03b5\n  cases' hu \u03b5 h\u03b5 with U hU\n  -- U : \u2115\n  -- hU : \u2200 (n : \u2115), n \u2265 U \u2192 |u n - 0| < \u03b5\n  cases' hv 1 zero_lt_one with V hV\n  -- V : \u2115\n  -- hV : \u2200 (n : \u2115), n \u2265 V \u2192 |v n - 0| < 1\n  let N := max U V\n  use N\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 N \u2192 |(u * v) n - 0| < \u03b5\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 N\n  -- \u22a2 |(u * v) n - 0| < \u03b5\n  specialize hU n (le_of_max_le_left hn)\n  -- hU : |u n - 0| < \u03b5\n  specialize hV n (le_of_max_le_right hn)\n  -- hV : |v n - 0| < 1\n  rw [sub_zero] at *\n  -- hU : |u n - 0| < \u03b5\n  -- hV : |v n - 0| < 1\n  -- \u22a2 |(u * v) n - 0| < \u03b5\n  calc |(u * v) n|\n       = |u n * v n|   := rfl\n     _ = |u n| * |v n| := abs_mul (u n) (v n)\n     _ < \u03b5 * 1         := mul_lt_mul'' hU hV (abs_nonneg (u n)) (abs_nonneg (v n))\n     _ = \u03b5             := mul_one \u03b5\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : limite u 0)\n  (hv : limite v 0)\n  : limite (u * v) 0 :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(u * v) n - 0| < \u03b5\n  cases' hu \u03b5 h\u03b5 with U hU\n  -- U : \u2115\n  -- hU : \u2200 (n : \u2115), n \u2265 U \u2192 |u n - 0| < \u03b5\n  cases' hv 1 (by linarith) with V hV\n  -- V : \u2115\n  -- hV : \u2200 (n : \u2115), n \u2265 V \u2192 |v n - 0| < 1\n  let N := max U V\n  use N\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 N \u2192 |(u * v) n - 0| < \u03b5\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 N\n  -- \u22a2 |(u * v) n - 0| < \u03b5\n  specialize hU n (le_of_max_le_left hn)\n  -- hU : |u n - 0| < \u03b5\n  specialize hV n (le_of_max_le_right hn)\n  -- hV : |v n - 0| < 1\n  rw [sub_zero] at *\n  -- hU : |u n| < \u03b5\n  -- hV : |v n| < 1\n  -- \u22a2 |(u * v) n| < \u03b5\n  calc |(u * v) n|\n       = |u n * v n|   := rfl\n     _ = |u n| * |v n| := abs_mul (u n) (v n)\n     _ < \u03b5 * 1         := by { apply mul_lt_mul'' hU hV <;> simp [abs_nonneg] }\n     _ = \u03b5             := mul_one \u03b5\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : limite u 0)\n  (hv : limite v 0)\n  : limite (u * v) 0 :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(u * v) n - 0| < \u03b5\n  cases' hu \u03b5 h\u03b5 with U hU\n  -- U : \u2115\n  -- hU : \u2200 (n : \u2115), n \u2265 U \u2192 |u n - 0| < \u03b5\n  cases' hv 1 (by linarith) with V hV\n  -- V : \u2115\n  -- hV : \u2200 (n : \u2115), n \u2265 V \u2192 |v n - 0| < 1\n  let N := max U V\n  use N\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 N \u2192 |(u * v) n - 0| < \u03b5\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 N\n  -- \u22a2 |(u * v) n - 0| < \u03b5\n  have hUN : U \u2264 N := le_max_left U V\n  have hVN : V \u2264 N := le_max_right U V\n  specialize hU n (by linarith)\n  -- hU : |u n - 0| < \u03b5\n  specialize hV n (by linarith)\n  -- hV : |v n - 0| < 1\n  rw [sub_zero] at *\n  -- hU : |u n| < \u03b5\n  -- hV : |v n| < 1\n  -- \u22a2 |(u * v) n| < \u03b5\n  rw [Pi.mul_apply]\n  -- \u22a2 |u n * v n| < \u03b5\n  rw [abs_mul]\n  -- \u22a2 |u n| * |v n| < \u03b5\n  convert mul_lt_mul'' hU hV _ _ using 2 <;> simp\n\n-- Lemas usados\n-- ============\n\n-- variable (a b c d : \u211d)\n-- variable (I : Type _)\n-- variable (f : I \u2192 Type _)\n-- #check (zero_lt_one : 0 < 1)\n-- #check (le_of_max_le_left : max a b \u2264 c \u2192 a \u2264 c)\n-- #check (le_of_max_le_right : max a b \u2264 c \u2192 b \u2264 c)\n-- #check (sub_zero a : a - 0 = a)\n-- #check (abs_mul a b : |a * b| = |a| * |b|)\n-- #check (mul_lt_mul'' : a < c \u2192 b < d \u2192 0 \u2264 a \u2192 0 \u2264 b \u2192 a * b < c * d)\n-- #check (abs_nonneg a : 0 \u2264 |a|)\n-- #check (mul_one a : a * 1 = 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\/Producto_de_sucesiones_convergentes_a_cero.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<h5>6.3. Demostraciones con Isabelle\/HOL<\/h5>\n<pre lang=\"isar\">\ntheory Producto_de_sucesiones_convergentes_a_cero\nimports Main HOL.Real\nbegin\n\ndefinition limite :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\"\n  where \"limite u c \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6u n - c\u00a6 < \u03b5)\"\n\nlemma\n  assumes \"limite u 0\"\n          \"limite v 0\"\n  shows   \"limite (\u03bb n. u n * v n) 0\"\nproof (unfold limite_def; intro allI impI)\n  fix \u03b5 :: real\n  assume  h\u03b5 : \"0 < \u03b5\"\n  then obtain U where hU : \"\u2200n\u2265U. \u00a6u n - 0\u00a6 < \u03b5\"\n    using assms(1) limite_def\n    by auto\n  obtain V where hV : \"\u2200n\u2265V. \u00a6v n - 0\u00a6 < 1\"\n    using h\u03b5 assms(2) limite_def\n    by fastforce\n  have \"\u2200n\u2265max U V. \u00a6u n * v n - 0\u00a6 < \u03b5\"\n  proof (intro allI impI)\n    fix n\n    assume hn : \"max U V \u2264 n\"\n    then have \"U \u2264 n\"\n      by simp\n    then have \"\u00a6u n - 0\u00a6 < \u03b5\"\n      using hU by blast\n    have hnV : \"V \u2264 n\"\n      using hn by simp\n    then have \"\u00a6v n - 0\u00a6 < 1\"\n      using hV by blast\n    have \"\u00a6u n * v n - 0\u00a6 = \u00a6(u n - 0) * (v n - 0)\u00a6\"\n      by simp\n    also have \"\u2026 = \u00a6u n - 0\u00a6 * \u00a6v n - 0\u00a6\"\n      by (simp add: abs_mult)\n    also have \"\u2026 < \u03b5 * 1\"\n      using \u2039\u00a6u n - 0\u00a6 < \u03b5\u203a \u2039\u00a6v n - 0\u00a6 < 1\u203a\n      by (rule abs_mult_less)\n    also have \"\u2026 = \u03b5\"\n      by simp\n    finally show \"\u00a6u n * v n - 0\u00a6 < \u03b5\"\n      by this\n  qed\n  then show \"\u2203k. \u2200n\u2265k. \u00a6u n * v n - 0\u00a6 < \u03b5\"\n    by (rule exI)\nqed\n\nend\n<\/pre>\n<p><a name=\"ej7\"><\/a><\/p>\n<h3>7. Teorema del emparedado<\/h3>\n<p>Demostrar con Lean4 el teorema del emparedado.<\/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 v w : \u2115 \u2192 \u211d)\nvariable (a : \u211d)\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n  fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| \u2264 \u03b5\n\nexample\n  (hu : limite u a)\n  (hw : limite w a)\n  (h1 : \u2200 n, u n \u2264 v n)\n  (h2 : \u2200 n, v n \u2264 w n) :\n  limite v a :=\nby sorry\n<\/pre>\n<h5>7.1. Demostraci\u00f3n en lenguaje natural<\/h5>\n<p>Tenemos que demostrar que para cada &#92;(\u03b5 > 0&#92;), existe un &#92;(N \u2208 \u2115&#92;) tal que<br \/>\n&#92;[ (\u2200 n \u2265 N)[|v(n) - a| \u2264 \u03b5] &#92;tag{1} &#92;]<\/p>\n<p>Puesto que el l\u00edmite de &#92;(u&#92;) es &#92;(a&#92;), existe un &#92;(U \u2208 \u2115&#92;) tal que<br \/>\n&#92;[ (\u2200 n \u2265 U)[|u(n) - a| \u2264 \u03b5] &#92;tag{2} &#92;]<br \/>\ny, puesto que el l\u00edmite de &#92;(w&#92;) es &#92;(a&#92;), existe un &#92;(W \u2208 \u2115&#92;) tal que<br \/>\n&#92;[ (\u2200 n \u2265 W)[|w(n) - a| \u2264 \u03b5] &#92;tag{3} &#92;]<br \/>\nSea &#92;(N = &#92;text{m\u00e1x}(U, W)&#92;). Veamos que se verifica (1). Para ello, sea &#92;(n \u2265 N&#92;). Entonces, &#92;(n \u2265 U&#92;), &#92;(n \u2265 W&#92;) y, por (2) y (3), se tiene que<br \/>\n&#92;begin{align}<br \/>\n    |u(n) - a| &amp;\u2264 \u03b5 &#92;tag{4} &#92;&#92;<br \/>\n    |w(n) - a| &amp;\u2264 \u03b5 &#92;tag{5}<br \/>\n&#92;end{align}<br \/>\nPara demostrar que<br \/>\n&#92;[ |v(n) - a| \u2264 \u03b5 &#92;]<br \/>\nbasta demostrar las siguientes desigualdades<br \/>\n&#92;begin{align}<br \/>\n    &amp;-\u03b5 \u2264 v(n) - a &#92;tag{6} &#92;&#92;<br \/>\n    &amp;v(n) - a \u2264 \u03b5  &#92;tag{7}<br \/>\n&#92;end{align}<br \/>\nLa demostraci\u00f3n de (6) es<br \/>\n&#92;begin{align}<br \/>\n   -\u03b5 &amp;\u2264 u(n) - a    &amp;&amp;&#92;text{[por (4)]} &#92;&#92;<br \/>\n      &amp;\u2264 v(n) - a    &amp;&amp;&#92;text{[por hip\u00f3tesis]}<br \/>\n&#92;end{align}<br \/>\nLa demostraci\u00f3n de (7) es<br \/>\n&#92;begin{align}<br \/>\n   v(n) - a &amp;\u2264 w(n) - a    &amp;&amp;&#92;text{[por hip\u00f3tesis]} &#92;&#92;<br \/>\n            &amp;\u2264 \u03b5           &amp;&amp;&#92;text{[por (5)]}<br \/>\n&#92;end{align}<\/p>\n<h5>7.2. Demostraciones con Lean4<\/h5>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (u v w : \u2115 \u2192 \u211d)\nvariable (a : \u211d)\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n  fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| \u2264 \u03b5\n\n-- Nota. En la demostraci\u00f3n se usar\u00e1 el siguiente lema:\nlemma max_ge_iff\n  {p q r : \u2115}\n  : r \u2265 max p q \u2194 r \u2265 p \u2227 r \u2265 q :=\n  max_le_iff\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : limite u a)\n  (hw : limite w a)\n  (h1 : \u2200 n, u n \u2264 v n)\n  (h2 : \u2200 n, v n \u2264 w n) :\n  limite v a :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |v n - a| \u2264 \u03b5\n  rcases hu \u03b5 h\u03b5 with \u27e8U, hU\u27e9\n  -- U : \u2115\n  -- hU : \u2200 (n : \u2115), n \u2265 U \u2192 |u n - a| \u2264 \u03b5\n  clear hu\n  rcases hw \u03b5 h\u03b5 with \u27e8W, hW\u27e9\n  -- W : \u2115\n  -- hW : \u2200 (n : \u2115), n \u2265 W \u2192 |w n - a| \u2264 \u03b5\n  clear hw h\u03b5\n  use max U W\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 max U W\n  -- \u22a2 |v n - a| \u2264 \u03b5\n  rw [max_ge_iff] at hn\n  -- hn : n \u2265 U \u2227 n \u2265 W\n  specialize hU n hn.1\n  -- hU : |u n - a| \u2264 \u03b5\n  specialize hW n hn.2\n  -- hW : |w n - a| \u2264 \u03b5\n  specialize h1 n\n  -- h1 : u n \u2264 v n\n  specialize h2 n\n  -- h2 : v n \u2264 w n\n  clear hn\n  rw [abs_le] at *\n  -- \u22a2 -\u03b5 \u2264 v n - a \u2227 v n - a \u2264 \u03b5\n  constructor\n  . -- \u22a2 -\u03b5 \u2264 v n - a\n    calc -\u03b5\n         \u2264 u n - a := hU.1\n       _ \u2264 v n - a := by linarith\n  . -- \u22a2 v n - a \u2264 \u03b5\n    calc v n - a\n         \u2264 w n - a := by linarith\n       _ \u2264 \u03b5       := hW.2\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (hu : limite u a)\n  (hw : limite w a)\n  (h1 : \u2200 n, u n \u2264 v n)\n  (h2 : \u2200 n, v n \u2264 w n) :\n  limite v a :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |v n - a| \u2264 \u03b5\n  rcases hu \u03b5 h\u03b5 with \u27e8U, hU\u27e9\n  -- U : \u2115\n  -- hU : \u2200 (n : \u2115), n \u2265 U \u2192 |u n - a| \u2264 \u03b5\n  clear hu\n  rcases hw \u03b5 h\u03b5 with \u27e8W, hW\u27e9\n  -- W : \u2115\n  -- hW : \u2200 (n : \u2115), n \u2265 W \u2192 |w n - a| \u2264 \u03b5\n  clear hw h\u03b5\n  use max U W\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 max U W\n  rw [max_ge_iff] at hn\n  -- hn : n \u2265 U \u2227 n \u2265 W\n  specialize hU n (by linarith)\n  -- hU : |u n - a| \u2264 \u03b5\n  specialize hW n (by linarith)\n  -- hW : |w n - a| \u2264 \u03b5\n  specialize h1 n\n  -- h1 : u n \u2264 v n\n  specialize h2 n\n  -- h2 : v n \u2264 w n\n  rw [abs_le] at *\n  -- \u22a2 -\u03b5 \u2264 v n - a \u2227 v n - a \u2264 \u03b5\n  constructor\n  . -- \u22a2 -\u03b5 \u2264 v n - a\n    linarith\n  . -- \u22a2 v n - a \u2264 \u03b5\n    linarith\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (hu : limite u a)\n  (hw : limite w a)\n  (h1 : \u2200 n, u n \u2264 v n)\n  (h2 : \u2200 n, v n \u2264 w n) :\n  limite v a :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |v n - a| \u2264 \u03b5\n  rcases hu \u03b5 h\u03b5 with \u27e8U, hU\u27e9\n  -- U : \u2115\n  -- hU : \u2200 (n : \u2115), n \u2265 U \u2192 |u n - a| \u2264 \u03b5\n  clear hu\n  rcases hw \u03b5 h\u03b5 with \u27e8W, hW\u27e9\n  -- W : \u2115\n  -- hW : \u2200 (n : \u2115), n \u2265 W \u2192 |w n - a| \u2264 \u03b5\n  clear hw h\u03b5\n  use max U W\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 max U W\n  -- \u22a2 |v n - a| \u2264 \u03b5\n  rw [max_ge_iff] at hn\n  -- hn : n \u2265 U \u2227 n \u2265 W\n  specialize hU n (by linarith)\n  -- hU : |u n - a| \u2264 \u03b5\n  specialize hW n (by linarith)\n  -- hW : |w n - a| \u2264 \u03b5\n  specialize h1 n\n  -- h1 : u n \u2264 v n\n  specialize h2 n\n  -- h2 : v n \u2264 w n\n  rw [abs_le] at *\n  -- hU : -\u03b5 \u2264 u n - a \u2227 u n - a \u2264 \u03b5\n  -- hW : -\u03b5 \u2264 w n - a \u2227 w n - a \u2264 \u03b5\n  -- \u22a2 -\u03b5 \u2264 v n - a \u2227 v n - a \u2264 \u03b5\n  constructor <;> linarith\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\/Teorema_del_emparedado.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<h5>7.3. Demostraciones con Isabelle\/HOL<\/h5>\n<pre lang=\"isar\">\ntheory Teorema_del_emparedado\nimports Main HOL.Real\nbegin\n\ndefinition limite :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\"\n  where \"limite u c \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6u n - c\u00a6 < \u03b5)\"\n\nlemma\n  assumes \"limite u a\"\n          \"limite w a\"\n          \"\u2200n. u n \u2264 v n\"\n          \"\u2200n. v n \u2264 w n\"\n  shows   \"limite v a\"\nproof (unfold limite_def; intro allI impI)\n  fix \u03b5 :: real\n  assume h\u03b5 : \"0 < \u03b5\"\n  obtain N where hN : \"\u2200n\u2265N. \u00a6u n - a\u00a6 < \u03b5\"\n    using assms(1) h\u03b5 limite_def\n    by auto\n  obtain N' where hN' : \"\u2200n\u2265N'. \u00a6w n - a\u00a6 < \u03b5\"\n    using assms(2) h\u03b5 limite_def\n    by auto\n  have \"\u2200n\u2265max N N'. \u00a6v n - a\u00a6 < \u03b5\"\n  proof (intro allI impI)\n    fix n\n    assume hn : \"n\u2265max N N'\"\n    have \"v n - a < \u03b5\"\n    proof -\n      have \"v n - a \u2264 w n - a\"\n        using assms(4) by simp\n      also have \"\u2026 \u2264 \u00a6w n - a\u00a6\"\n        by simp\n      also have \"\u2026 < \u03b5\"\n        using hN' hn by auto\n      finally show \"v n - a < \u03b5\" .\n    qed\n    moreover\n    have \"-(v n - a) < \u03b5\"\n    proof -\n      have \"-(v n - a) \u2264 -(u n - a)\"\n        using assms(3) by auto\n      also have \"\u2026 \u2264 \u00a6u n - a\u00a6\"\n        by simp\n      also have \"\u2026 < \u03b5\"\n        using hN hn by auto\n      finally show \"-(v n - a) < \u03b5\" .\n    qed\n    ultimately show \"\u00a6v n - a\u00a6 < \u03b5\"\n      by (simp only: abs_less_iff)\n  qed\n  then show \"\u2203k. \u2200n\u2265k. \u00a6v n - a\u00a6 < \u03b5\"\n    by (rule exI)\nqed\n\nend\n<\/pre>\n<p><a name=\"ej8\"><\/a><\/p>\n<h3>8. Si s \u2286 t, entonces s \u2229 u \u2286 t \u2229 u<\/h3>\n<p>Demostrar con Lean4 que \"Si &#92;(s \u2286 t&#92;), entonces &#92;(s \u2229 u \u2286 t \u2229 u&#92;)\".<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\nopen Set\nvariable {\u03b1 : Type}\nvariable (s t u : Set \u03b1)\n\nexample\n  (h : s \u2286 t)\n  : s \u2229 u \u2286 t \u2229 u :=\nby sorry\n<\/pre>\n<h5>8.1. Demostraci\u00f3n en lenguaje natural<\/h5>\n<p>Sea &#92;(x \u2208 s \u2229 u&#92;). Entonces, se tiene que<br \/>\n&#92;begin{align}<br \/>\n  &amp;x \u2208 s &#92;tag{1} &#92;&#92;<br \/>\n  &amp;x \u2208 u &#92;tag{2}<br \/>\n&#92;end{align}<br \/>\nDe (1) y &#92;(s \u2286 t&#92;), se tiene que<br \/>\n&#92;[ x \u2208 t &#92;tag{3} &#92;]<br \/>\nDe (3) y (2) se tiene que<br \/>\n&#92;[ x \u2208 t \u2229 u &#92;]<br \/>\nque es lo que ten\u00edamos que demostrar.<\/p>\n<h5>8.2. Demostraciones con Lean4<\/h5>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 : Type}\nvariable (s t u : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : s \u2286 t)\n  : s \u2229 u \u2286 t \u2229 u :=\nby\n  rw [subset_def]\n  -- \u22a2 \u2200 (x : \u03b1), x \u2208 s \u2229 u \u2192 x \u2208 t \u2229 u\n  intros x h1\n  -- x : \u03b1\n  -- h1 : x \u2208 s \u2229 u\n  -- \u22a2 x \u2208 t \u2229 u\n  rcases h1 with \u27e8xs, xu\u27e9\n  -- xs : x \u2208 s\n  -- xu : x \u2208 u\n  constructor\n  . -- \u22a2 x \u2208 t\n    rw [subset_def] at h\n    -- h : \u2200 (x : \u03b1), x \u2208 s \u2192 x \u2208 t\n    apply h\n    -- \u22a2 x \u2208 s\n    exact xs\n  . -- \u22a2 x \u2208 u\n    exact xu\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : s \u2286 t)\n  : s \u2229 u \u2286 t \u2229 u :=\nby\n  rw [subset_def]\n  -- \u22a2 \u2200 (x : \u03b1), x \u2208 s \u2229 u \u2192 x \u2208 t \u2229 u\n  rintro x \u27e8xs, xu\u27e9\n  -- x : \u03b1\n  -- xs : x \u2208 s\n  -- xu : x \u2208 u\n  rw [subset_def] at h\n  -- h : \u2200 (x : \u03b1), x \u2208 s \u2192 x \u2208 t\n  exact \u27e8h x xs, xu\u27e9\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : s \u2286 t)\n  : s \u2229 u \u2286 t \u2229 u :=\nby\n  simp only [subset_def]\n  -- \u22a2 \u2200 (x : \u03b1), x \u2208 s \u2229 u \u2192 x \u2208 t \u2229 u\n  rintro x \u27e8xs, xu\u27e9\n  -- x : \u03b1\n  -- xs : x \u2208 s\n  -- xu : x \u2208 u\n  rw [subset_def] at h\n  -- h : \u2200 (x : \u03b1), x \u2208 s \u2192 x \u2208 t\n  exact \u27e8h _ xs, xu\u27e9\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : s \u2286 t)\n  : s \u2229 u \u2286 t \u2229 u :=\nby\n  intros x xsu\n  -- x : \u03b1\n  -- xsu : x \u2208 s \u2229 u\n  -- \u22a2 x \u2208 t \u2229 u\n  exact \u27e8h xsu.1, xsu.2\u27e9\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : s \u2286 t)\n  : s \u2229 u \u2286 t \u2229 u :=\nby\n  rintro x \u27e8xs, xu\u27e9\n  -- xs : x \u2208 s\n  -- xu : x \u2208 u\n  -- \u22a2 x \u2208 t \u2229 u\n  exact \u27e8h xs, xu\u27e9\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : s \u2286 t)\n  : s \u2229 u \u2286 t \u2229 u :=\n  fun _ \u27e8xs, xu\u27e9 \u21a6  \u27e8h xs, xu\u27e9\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : s \u2286 t)\n  : s \u2229 u \u2286 t \u2229 u :=\n  inter_subset_inter_left u h\n\n-- Lema usado\n-- ==========\n\n-- #check (inter_subset_inter_left u : s \u2286 t \u2192 s \u2229 u \u2286 t \u2229 u)\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\/Propiedad_de_monotonia_de_la_interseccion.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<h5>8.3. Demostraciones con Isabelle\/HOL<\/h5>\n<pre lang=\"isar\">\ntheory Propiedad_de_monotonia_de_la_interseccion\nimports Main\nbegin\n\n(* 1\u00aa soluci\u00f3n *)\nlemma\n  assumes \"s \u2286 t\"\n  shows   \"s \u2229 u \u2286 t \u2229 u\"\nproof (rule subsetI)\n  fix x\n  assume hx: \"x \u2208 s \u2229 u\"\n  have xs: \"x \u2208 s\"\n    using hx\n    by (simp only: IntD1)\n  then have xt: \"x \u2208 t\"\n    using assms\n    by (simp only: subset_eq)\n  have xu: \"x \u2208 u\"\n    using hx\n    by (simp only: IntD2)\n  show \"x \u2208 t \u2229 u\"\n    using xt xu\n    by (simp only: Int_iff)\nqed\n\n(* 2 soluci\u00f3n *)\nlemma\n  assumes \"s \u2286 t\"\n  shows   \"s \u2229 u \u2286 t \u2229 u\"\nproof\n  fix x\n  assume hx: \"x \u2208 s \u2229 u\"\n  have xs: \"x \u2208 s\"\n    using hx\n    by simp\n  then have xt: \"x \u2208 t\"\n    using assms\n    by auto\n  have xu: \"x \u2208 u\"\n    using hx\n    by simp\n  show \"x \u2208 t \u2229 u\"\n    using xt xu\n    by simp\nqed\n\n(* 3\u00aa soluci\u00f3n *)\nlemma\n  assumes \"s \u2286 t\"\n  shows   \"s \u2229 u \u2286 t \u2229 u\"\nusing assms\nby auto\n\n(* 4\u00aa soluci\u00f3n *)\nlemma\n  \"s \u2286 t \u27f9 s \u2229 u \u2286 t \u2229 u\"\nby auto\n\nend\n<\/pre>\n<p><a name=\"ej9\"><\/a><\/p>\n<h3>9. s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u)<\/h3>\n<p>Demostrar con Lean4 que &#92;(s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u)&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\nopen Set\nvariable {\u03b1 : Type}\nvariable (s t u : Set \u03b1)\n\nexample :\n  s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u) :=\nby sorry\n<\/pre>\n<h5>9.1. Demostraci\u00f3n en lenguaje natural<\/h5>\n<p>Sea &#92;(x \u2208 s \u2229 (t \u222a u)&#92;). Entonces se tiene que<br \/>\n&#92;begin{align}<br \/>\n   &amp;x \u2208 s     &#92;tag{1} &#92;&#92;<br \/>\n   &amp;x \u2208 t \u222a u &#92;tag{2}<br \/>\n&#92;end{align}<br \/>\nLa relaci\u00f3n (2) da lugar a dos casos.<\/p>\n<p>Caso 1: Supongamos que &#92;(x \u2208 t&#92;). Entonces, por (1), &#92;(x \u2208 s \u2229 t&#92;) y, por tanto, &#92;(x \u2208 (s \u2229 t) \u222a (s \u2229 u)&#92;).<\/p>\n<p>Caso 2: Supongamos que &#92;(x \u2208 u&#92;). Entonces, por (1), &#92;(x \u2208 s \u2229 u&#92;) y, por tanto, &#92;(x \u2208 (s \u2229 t) \u222a (s \u2229 u)&#92;).<\/p>\n<h5>9.2. Demostraciones con Lean4<\/h5>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 : Type}\nvariable (s t u : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u) :=\nby\n  intros x hx\n  -- x : \u03b1\n  -- hx : x \u2208 s \u2229 (t \u222a u)\n  -- \u22a2 x \u2208 s \u2229 t \u222a s \u2229 u\n  rcases hx with \u27e8hxs, hxtu\u27e9\n  -- hxs : x \u2208 s\n  -- hxtu : x \u2208 t \u222a u\n  rcases hxtu with (hxt | hxu)\n  . -- hxt : x \u2208 t\n    left\n    -- \u22a2 x \u2208 s \u2229 t\n    constructor\n    . -- \u22a2 x \u2208 s\n      exact hxs\n    . -- hxt : x \u2208 t\n      exact hxt\n  . -- hxu : x \u2208 u\n    right\n    -- \u22a2 x \u2208 s \u2229 u\n    constructor\n    . -- \u22a2 x \u2208 s\n      exact hxs\n    . -- \u22a2 x \u2208 u\n      exact hxu\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u) :=\nby\n  rintro x \u27e8hxs, hxt | hxu\u27e9\n  -- x : \u03b1\n  -- hxs : x \u2208 s\n  -- \u22a2 x \u2208 s \u2229 t \u222a s \u2229 u\n  . -- hxt : x \u2208 t\n    left\n    -- \u22a2 x \u2208 s \u2229 t\n    exact \u27e8hxs, hxt\u27e9\n  . -- hxu : x \u2208 u\n    right\n    -- \u22a2 x \u2208 s \u2229 u\n    exact \u27e8hxs, hxu\u27e9\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u) :=\nby\n  rintro x \u27e8hxs, hxt | hxu\u27e9\n  -- x : \u03b1\n  -- hxs : x \u2208 s\n  -- \u22a2 x \u2208 s \u2229 t \u222a s \u2229 u\n  . -- hxt : x \u2208 t\n    exact Or.inl \u27e8hxs, hxt\u27e9\n  . -- hxu : x \u2208 u\n    exact Or.inr \u27e8hxs, hxu\u27e9\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u) :=\nby\n  intro x hx\n  -- x : \u03b1\n  -- hx : x \u2208 s \u2229 (t \u222a u)\n  -- \u22a2 x \u2208 s \u2229 t \u222a s \u2229 u\n  aesop\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u) :=\nby rw [inter_union_distrib_left]\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\/Propiedad_semidistributiva_de_la_interseccion_sobre_la_union.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<h5>9.3. Demostraciones con Isabelle\/HOL<\/h5>\n<pre lang=\"isar\">\ntheory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\nlemma \"s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u)\"\nproof (rule subsetI)\n  fix x\n  assume hx : \"x \u2208 s \u2229 (t \u222a u)\"\n  then have xs : \"x \u2208 s\"\n    by (simp only: IntD1)\n  have xtu: \"x \u2208 t \u222a u\"\n    using hx\n    by (simp only: IntD2)\n  then have \"x \u2208 t \u2228 x \u2208 u\"\n    by (simp only: Un_iff)\n  then show \" x \u2208 s \u2229 t \u222a s \u2229 u\"\n  proof (rule disjE)\n    assume xt : \"x \u2208 t\"\n    have xst : \"x \u2208 s \u2229 t\"\n      using xs xt by (simp only: Int_iff)\n    then show \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n      by (simp only: UnI1)\n  next\n    assume xu : \"x \u2208 u\"\n    have xst : \"x \u2208 s \u2229 u\"\n      using xs xu by (simp only: Int_iff)\n    then show \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n      by (simp only: UnI2)\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\nlemma \"s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u)\"\nproof\n  fix x\n  assume hx : \"x \u2208 s \u2229 (t \u222a u)\"\n  then have xs : \"x \u2208 s\"\n    by simp\n  have xtu: \"x \u2208 t \u222a u\"\n    using hx\n    by simp\n  then have \"x \u2208 t \u2228 x \u2208 u\"\n    by simp\n  then show \" x \u2208 s \u2229 t \u222a s \u2229 u\"\n  proof\n    assume xt : \"x \u2208 t\"\n    have xst : \"x \u2208 s \u2229 t\"\n      using xs xt\n      by simp\n    then show \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n      by simp\n  next\n    assume xu : \"x \u2208 u\"\n    have xst : \"x \u2208 s \u2229 u\"\n      using xs xu\n      by simp\n    then show \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n      by simp\n  qed\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\nlemma \"s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u)\"\nproof (rule subsetI)\n  fix x\n  assume hx : \"x \u2208 s \u2229 (t \u222a u)\"\n  then have xs : \"x \u2208 s\"\n    by (simp only: IntD1)\n  have xtu: \"x \u2208 t \u222a u\"\n    using hx\n    by (simp only: IntD2)\n  then show \" x \u2208 s \u2229 t \u222a s \u2229 u\"\n  proof (rule UnE)\n    assume xt : \"x \u2208 t\"\n    have xst : \"x \u2208 s \u2229 t\"\n      using xs xt\n      by (simp only: Int_iff)\n    then show \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n      by (simp only: UnI1)\n  next\n    assume xu : \"x \u2208 u\"\n    have xst : \"x \u2208 s \u2229 u\"\n      using xs xu\n      by (simp only: Int_iff)\n    then show \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n      by (simp only: UnI2)\n  qed\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\nlemma \"s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u)\"\nproof\n  fix x\n  assume hx : \"x \u2208 s \u2229 (t \u222a u)\"\n  then have xs : \"x \u2208 s\"\n    by simp\n  have xtu: \"x \u2208 t \u222a u\"\n    using hx\n    by simp\n  then show \" x \u2208 s \u2229 t \u222a s \u2229 u\"\n  proof (rule UnE)\n    assume xt : \"x \u2208 t\"\n    have xst : \"x \u2208 s \u2229 t\"\n      using xs xt\n      by simp\n    then show \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n      by simp\n  next\n    assume xu : \"x \u2208 u\"\n    have xst : \"x \u2208 s \u2229 u\"\n      using xs xu by simp\n    then show \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n      by simp\n  qed\nqed\n\n(* 5\u00aa demostraci\u00f3n *)\nlemma \"s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u)\"\nby (simp only: Int_Un_distrib)\n\n(* 6\u00aa demostraci\u00f3n *)\nlemma \"s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u)\"\nby auto\n\nend\n<\/pre>\n<p><a name=\"ej10\"><\/a><\/p>\n<h3>10. (s \\ t) \\ u \u2286 s \\ (t \u222a u)<\/h3>\n<p>Demostrar con Lean4 que<br \/>\n&#92;[ (s \\setminus t) \\setminus u \u2286 s \\setminus (t \u222a u) &#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nopen Set\nvariable {\u03b1 : Type}\nvariable (s t u : Set \u03b1)\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby sorry\n<\/pre>\n<h5>10.1. Demostraci\u00f3n en lenguaje natural<\/h5>\n<p>Sea &#92;(x \u2208 (s \\setminus t) \\setminus u&#92;). Entonces, se tiene que<br \/>\n&#92;begin{align}<br \/>\n   &amp;x \u2208 s &#92;tag{1} &#92;&#92;<br \/>\n   &amp;x \u2209 t &#92;tag{2} &#92;&#92;<br \/>\n   &amp;x \u2209 u &#92;tag{3}<br \/>\n&#92;end{align}<br \/>\nTenemos que demostrar que<br \/>\n&#92;[ x \u2208 s \\setminus (t \u222a u) &#92;]<br \/>\npero, por (1), se reduce a<br \/>\n&#92;[ x \u2209 t \u222a u &#92;]<br \/>\nque se verifica por (2) y (3).<\/p>\n<h5>10.2. Demostraciones con Lean4<\/h5>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nopen Set\n\nvariable {\u03b1 : Type}\nvariable (s t u : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby\n  intros x hx\n  -- x : \u03b1\n  -- hx : x \u2208 (s \\ t) \\ u\n  -- \u22a2 x \u2208 s \\ (t \u222a u)\n  rcases hx with \u27e8hxst, hxnu\u27e9\n  -- hxst : x \u2208 s \\ t\n  -- hxnu : \u00acx \u2208 u\n  rcases hxst with \u27e8hxs, hxnt\u27e9\n  -- hxs : x \u2208 s\n  -- hxnt : \u00acx \u2208 t\n  constructor\n  . -- \u22a2 x \u2208 s\n    exact hxs\n  . -- \u22a2 \u00acx \u2208 t \u222a u\n    by_contra hxtu\n    -- hxtu : x \u2208 t \u222a u\n    -- \u22a2 False\n    rcases hxtu with (hxt | hxu)\n    . -- hxt : x \u2208 t\n      apply hxnt\n      -- \u22a2 x \u2208 t\n      exact hxt\n    . -- hxu : x \u2208 u\n      apply hxnu\n      -- \u22a2 x \u2208 u\n      exact hxu\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby\n  rintro x \u27e8\u27e8hxs, hxnt\u27e9, hxnu\u27e9\n  -- x : \u03b1\n  -- hxnu : \u00acx \u2208 u\n  -- hxs : x \u2208 s\n  -- hxnt : \u00acx \u2208 t\n  -- \u22a2 x \u2208 s \\ (t \u222a u)\n  constructor\n  . -- \u22a2 x \u2208 s\n    exact hxs\n  . -- \u22a2 \u00acx \u2208 t \u222a u\n    by_contra hxtu\n    -- hxtu : x \u2208 t \u222a u\n    -- \u22a2 False\n    rcases hxtu with (hxt | hxu)\n    . -- hxt : x \u2208 t\n      exact hxnt hxt\n    . -- hxu : x \u2208 u\n      exact hxnu hxu\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby\n  rintro x \u27e8\u27e8xs, xnt\u27e9, xnu\u27e9\n  -- x : \u03b1\n  -- xnu : \u00acx \u2208 u\n  -- xs : x \u2208 s\n  -- xnt : \u00acx \u2208 t\n  -- \u22a2 x \u2208 s \\ (t \u222a u)\n  use xs\n  -- \u22a2 \u00acx \u2208 t \u222a u\n  rintro (xt | xu)\n  . -- xt : x \u2208 t\n    -- \u22a2 False\n    contradiction\n  . -- xu : x \u2208 u\n    -- \u22a2 False\n    contradiction\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby\n  rintro x \u27e8\u27e8xs, xnt\u27e9, xnu\u27e9\n  -- x : \u03b1\n  -- xnu : \u00acx \u2208 u\n  -- xs : x \u2208 s\n  -- xnt : \u00acx \u2208 t\n  -- \u22a2 x \u2208 s \\ (t \u222a u)\n  use xs\n  -- \u22a2 \u00acx \u2208 t \u222a u\n  rintro (xt | xu) <;> contradiction\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby\n  intro x xstu\n  -- x : \u03b1\n  -- xstu : x \u2208 (s \\ t) \\ u\n  -- \u22a2 x \u2208 s \\ (t \u222a u)\n  simp at *\n  -- \u22a2 x \u2208 s \u2227 \u00ac(x \u2208 t \u2228 x \u2208 u)\n  aesop\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby\n  intro x xstu\n  -- x : \u03b1\n  -- xstu : x \u2208 (s \\ t) \\ u\n  -- \u22a2 x \u2208 s \\ (t \u222a u)\n  aesop\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby rw [diff_diff]\n\n-- Lema usado\n-- ==========\n\n-- #check (diff_diff : (s \\ t) \\ u = s \\ (t \u222a u))\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\/Diferencia_de_diferencia_de_conjuntos.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<h5>10.3. Demostraciones con Isabelle\/HOL<\/h5>\n<pre lang=\"isar\">\ntheory Diferencia_de_diferencia_de_conjuntos\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\nlemma \"(s - t) - u \u2286 s - (t \u222a u)\"\nproof (rule subsetI)\n  fix x\n  assume hx : \"x \u2208 (s - t) - u\"\n  then show \"x \u2208 s - (t \u222a u)\"\n  proof (rule DiffE)\n    assume xst : \"x \u2208 s - t\"\n    assume xnu : \"x \u2209 u\"\n    note xst\n    then show \"x \u2208 s - (t \u222a u)\"\n    proof (rule DiffE)\n      assume xs : \"x \u2208 s\"\n      assume xnt : \"x \u2209 t\"\n      have xntu : \"x \u2209 t \u222a u\"\n      proof (rule notI)\n        assume xtu : \"x \u2208 t \u222a u\"\n        then show False\n        proof (rule UnE)\n          assume xt : \"x \u2208 t\"\n          with xnt show False\n            by (rule notE)\n        next\n          assume xu : \"x \u2208 u\"\n          with xnu show False\n            by (rule notE)\n        qed\n      qed\n      show \"x \u2208 s - (t \u222a u)\"\n        using xs xntu by (rule DiffI)\n    qed\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\nlemma \"(s - t) - u \u2286 s - (t \u222a u)\"\nproof\n  fix x\n  assume hx : \"x \u2208 (s - t) - u\"\n  then have xst : \"x \u2208 (s - t)\"\n    by simp\n  then have xs : \"x \u2208 s\"\n    by simp\n  have xnt : \"x \u2209 t\"\n    using xst by simp\n  have xnu : \"x \u2209 u\"\n    using hx by simp\n  have xntu : \"x \u2209 t \u222a u\"\n    using xnt xnu by simp\n  then show \"x \u2208 s - (t \u222a u)\"\n    using xs by simp\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\nlemma \"(s - t) - u \u2286 s - (t \u222a u)\"\nproof\n  fix x\n  assume \"x \u2208 (s - t) - u\"\n  then show \"x \u2208 s - (t \u222a u)\"\n     by simp\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\nlemma \"(s - t) - u \u2286 s - (t \u222a u)\"\nby auto\n\nend\n<\/pre>\n<p><a name=\"ej11\"><\/a><\/p>\n<h3>11. (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)<\/h3>\n<p>Demostrar con Lean4 que<br \/>\n&#92;[ (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u) &#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nopen Set\nvariable {\u03b1 : Type}\nvariable (s t u : Set \u03b1)\n\nexample : (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u):=\nby sorry\n<\/pre>\n<h5>11.1. Demostraci\u00f3n en lenguaje natural<\/h5>\n<p>Sea &#92;(x \u2208 (s \u2229 t) \u222a (s \u2229 u)&#92;). Entonces son posibles dos casos.<\/p>\n<p>1\u00ba caso: Supongamos que &#92;(x \u2208 s \u2229 t&#92;). Entonces, &#92;(x \u2208 s&#92;) y &#92;(x \u2208 t&#92;) (y, por tanto, &#92;(x \u2208 t \u222a u&#92;)). Luego, &#92;(x \u2208 s \u2229 (t \u222a u)&#92;).<\/p>\n<p>2\u00ba caso: Supongamos que &#92;(x \u2208 s \u2229 u&#92;). Entonces, &#92;(x \u2208 s&#92;) y &#92;(x \u2208 u&#92;) (y, por tanto, &#92;(x \u2208 t \u222a u&#92;)). Luego, &#92;(x \u2208 s \u2229 (t \u222a u)&#92;).<\/p>\n<h5>11.2. Demostraciones con Lean4<\/h5>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nopen Set\n\nvariable {\u03b1 : Type}\nvariable (s t u : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u):=\nby\n  intros x hx\n  -- x : \u03b1\n  -- hx : x \u2208 s \u2229 t \u222a s \u2229 u\n  -- \u22a2 x \u2208 s \u2229 (t \u222a u)\n  rcases hx with (xst | xsu)\n  . -- xst : x \u2208 s \u2229 t\n    constructor\n    . -- \u22a2 x \u2208 s\n      exact xst.1\n    . -- \u22a2 x \u2208 t \u222a u\n      left\n      -- \u22a2 x \u2208 t\n      exact xst.2\n  . -- xsu : x \u2208 s \u2229 u\n    constructor\n    . -- \u22a2 x \u2208 s\n      exact xsu.1\n    . -- \u22a2 x \u2208 t \u222a u\n      right\n      -- \u22a2 x \u2208 u\n      exact xsu.2\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u):=\nby\n  rintro x (\u27e8xs, xt\u27e9 | \u27e8xs, xu\u27e9)\n  . -- x : \u03b1\n    -- xs : x \u2208 s\n    -- xt : x \u2208 t\n    -- \u22a2 x \u2208 s \u2229 (t \u222a u)\n    use xs\n    -- \u22a2 x \u2208 t \u222a u\n    left\n    -- \u22a2 x \u2208 t\n    exact xt\n  . -- x : \u03b1\n    -- xs : x \u2208 s\n    -- xu : x \u2208 u\n    -- \u22a2 x \u2208 s \u2229 (t \u222a u)\n    use xs\n    -- \u22a2 x \u2208 t \u222a u\n    right\n    -- \u22a2 x \u2208 u\n    exact xu\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u):=\nby rw [inter_distrib_left s t u]\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u):=\nby\n  intros x hx\n  -- x : \u03b1\n  -- hx : x \u2208 s \u2229 t \u222a s \u2229 u\n  -- \u22a2 x \u2208 s \u2229 (t \u222a u)\n  aesop\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\/Propiedad_semidistributiva_de_la_interseccion_sobre_la_union_2.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<h5>11.3. Demostraciones con Isabelle\/HOL<\/h5>\n<pre lang=\"isar\">\ntheory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union_2\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\nlemma \"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)\"\nproof (rule subsetI)\n  fix x\n  assume \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n  then show \"x \u2208 s \u2229 (t \u222a u)\"\n  proof (rule UnE)\n    assume xst : \"x \u2208 s \u2229 t\"\n    then have xs : \"x \u2208 s\"\n      by (simp only: IntD1)\n    have xt : \"x \u2208 t\"\n      using xst by (simp only: IntD2)\n    then have xtu : \"x \u2208 t \u222a u\"\n      by (simp only: UnI1)\n    show \"x \u2208 s \u2229 (t \u222a u)\"\n      using xs xtu by (simp only: IntI)\n  next\n    assume xsu : \"x \u2208 s \u2229 u\"\n    then have xs : \"x \u2208 s\"\n      by (simp only: IntD1)\n    have xt : \"x \u2208 u\"\n      using xsu by (simp only: IntD2)\n    then have xtu : \"x \u2208 t \u222a u\"\n      by (simp only: UnI2)\n    show \"x \u2208 s \u2229 (t \u222a u)\"\n      using xs xtu by (simp only: IntI)\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\nlemma \"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)\"\nproof\n  fix x\n  assume \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n  then show \"x \u2208 s \u2229 (t \u222a u)\"\n  proof\n    assume xst : \"x \u2208 s \u2229 t\"\n    then have xs : \"x \u2208 s\"\n      by simp\n    have xt : \"x \u2208 t\"\n      using xst by simp\n    then have xtu : \"x \u2208 t \u222a u\"\n      by simp\n    show \"x \u2208 s \u2229 (t \u222a u)\"\n      using xs xtu by simp\n  next\n    assume xsu : \"x \u2208 s \u2229 u\"\n    then have xs : \"x \u2208 s\"\n      by (simp only: IntD1)\n    have xt : \"x \u2208 u\"\n      using xsu by simp\n    then have xtu : \"x \u2208 t \u222a u\"\n      by simp\n    show \"x \u2208 s \u2229 (t \u222a u)\"\n      using xs xtu by simp\n  qed\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\nlemma \"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)\"\nproof\n  fix x\n  assume \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n  then show \"x \u2208 s \u2229 (t \u222a u)\"\n  proof\n    assume \"x \u2208 s \u2229 t\"\n    then show \"x \u2208 s \u2229 (t \u222a u)\"\n      by simp\n  next\n    assume \"x \u2208 s \u2229 u\"\n    then show \"x \u2208 s \u2229 (t \u222a u)\"\n      by simp\n  qed\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\nlemma \"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)\"\nproof\n  fix x\n  assume \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n  then show \"x \u2208 s \u2229 (t \u222a u)\"\n    by auto\nqed\n\n(* 5\u00aa demostraci\u00f3n *)\nlemma \"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)\"\nby auto\n\n(* 6\u00aa demostraci\u00f3n *)\nlemma \"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)\"\nby (simp only: distrib_inf_le)\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>Estas 3 \u00faltimas semanas he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. Si la sucesi\u00f3n u converge a a y la v a b, entonces u+v converge a a+b 2. Unicidad del l\u00edmite de las sucesiones convergentes 3. Si el l\u00edmite de la sucesi\u00f3n u\u2099 es a y c \u2208&#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":[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\/8144"}],"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=8144"}],"version-history":[{"count":6,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8144\/revisions"}],"predecessor-version":[{"id":8151,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8144\/revisions\/8151"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8144"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8144"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8144"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}