{"id":8098,"date":"2024-02-03T18:18:15","date_gmt":"2024-02-03T17:18:15","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8098"},"modified":"2024-02-03T18:39:19","modified_gmt":"2024-02-03T17:39:19","slug":"03-feb-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/03-feb-24\/","title":{"rendered":"La semana en Calculemus (3 de febrero de 2024)"},"content":{"rendered":"\n<p>Esta semana he publicado en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/\">Calculemus<\/a> las demostraciones con Lean4 de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. La ra\u00edz cuadrada de 2 es irracional<\/a><\/li>\n<li><a href=\"#ej2\">2. Las funciones f(x,y) = (x + y)\u00b2 y g(x,y) = x\u00b2 + 2xy + y\u00b2 son iguales<\/a><\/li>\n<li><a href=\"#ej3\">3. En \u211d, |a| = |a &#8211; b + b|<\/a><\/li>\n<li><a href=\"#ej4\">4. En \u211d, si 1 &lt; a, entonces a &lt; aa<\/a><\/li>\n<li><a href=\"#ej5\">5. La sucesi\u00f3n constante s\u2099 = c converge a c<\/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. La ra\u00edz cuadrada de 2 es irracional<\/h3>\n<p>Demostrar con Lean4 que la ra\u00edz cuadrada de 2 es irracional; es decir, que no existen &#92;(m, n \u2208 \u2115&#92;) tales que &#92;(m&#92;) y &#92;(n&#92;) son coprimos (es decir, que no tienen factores comunes distintos de uno) y &#92;(m\u00b2 = 2n\u00b2&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nimport Mathlib.Data.Nat.Prime\nimport Std.Data.Nat.Gcd\nopen Nat\nvariable {m n : \u2115}\n\nexample : \u00ac\u2203 m n, coprime m n \u2227 m ^ 2 = 2 * n ^ 2 :=\nby sorry\n<\/pre>\n<p><b>1. Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Usaremos el lema del ejercicio anterior:<br \/>\n&#92;[ (\u2200 n \u2208 \u2115)[2 \u2223 n\u00b2 \u2192 2 | n] &#92;]<\/p>\n<p>Supongamos que existen existen &#92;(m, n \u2208 \u2115&#92;) tales que &#92;(m&#92;) y &#92;(n&#92;) son coprimos y &#92;(m\u00b2 = 2n\u00b2&#92;) y tenemos que demostrar una contradicci\u00f3n. Puesto que 2  divide a 1, para tener la contradicci\u00f3n basta demostrar que 2 divide a 1 y (ya que &#92;(m&#92;) y &#92;(n&#92;) son coprimos); para ello es suficiente demostrar que 2 divide al m\u00e1ximo com\u00fan divisor de &#92;(m&#92;) y &#92;(n&#92;). En definitiva, basta demostrar que 2 divide a &#92;(m&#92;) y a &#92;(n&#92;).<\/p>\n<p>La demostraci\u00f3n de que 2 divide a &#92;(m&#92;) es<br \/>\n&#92;begin{align}<br \/>\n   m\u00b2 = 2n\u00b2 &amp;\u27f9 2 | m\u00b2   &#92;&#92;<br \/>\n            &amp;\u27f9 2 | m    &amp;&amp;&#92;text{[por el lema]}<br \/>\n&#92;end{align}<\/p>\n<p>Para demostrar que 2 divide a &#92;(n&#92;), observamos que, puesto que 2 divide a &#92;(m&#92;), existe un &#92;(k \u2208 \u2115&#92;) tal que &#92;(m = 2k&#92;). Sustituyendo en<br \/>\n&#92;[ m\u00b2 = 2n\u00b2 &#92;]<br \/>\nse tiene<br \/>\n&#92;[ (2k)\u00b2 = 2n\u00b2 &#92;]<br \/>\nSimplificando, queda<br \/>\n&#92;[ 2k = n\u00b2 &#92;]<br \/>\nPor tanto, 2 divide a &#92;(n\u00b2&#92;) y, por el lema, 2 divide a &#92;(n&#92;).<\/p>\n<p><b>2. Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nimport Mathlib.Data.Nat.Prime\nimport Std.Data.Nat.Gcd\nopen Nat\nvariable {m n : \u2115}\n\nlemma par_si_cuadrado_par\n  (h : 2 \u2223 n ^ 2)\n  : 2 \u2223 n :=\nby\n  rw [pow_two] at h\n  -- h : 2 \u2223 n * n\n  have h2 : 2 \u2223 n \u2228 2 \u2223 n := (Prime.dvd_mul prime_two).mp h\n  tauto\n\nexample : \u00ac\u2203 m n, coprime m n \u2227 m ^ 2 = 2 * n ^ 2 :=\nby\n  rintro \u27e8m, n, \u27e8h1, h2\u27e9\u27e9\n  -- m n : \u2115\n  -- h1 : coprime m n\n  -- h2 : m ^ 2 = 2 * n ^ 2\n  -- \u22a2 False\n  have h3 : \u00ac(2 \u2223 1) := by norm_num\n  have h4 : 2 \u2223 1 := by\n    have h5 : Nat.gcd m n = 1 := h1\n    rw [\u2190 h5]\n    -- \u22a2 2 \u2223 Nat.gcd m n\n    have h6 : 2 \u2223 m := by\n      apply par_si_cuadrado_par\n      -- \u22a2 2 \u2223 m ^ 2\n      rw [h2]\n      -- \u22a2 2 \u2223 2 * n ^ 2\n      exact Nat.dvd_mul_right 2 (n ^ 2)\n    have h7 : 2 \u2223 n := by\n      have h8 : \u2203 k, m = 2 * k := h6\n      rcases h8 with \u27e8k, h9\u27e9\n      -- k : \u2115\n      -- h9 : m = 2 * k\n      have h10 : 2 * k ^ 2 = n ^ 2 := by\n        have h10a : 2 * (2 * k ^ 2) = 2 * n ^ 2 := calc\n          2 * (2 * k ^ 2) = (2 * k) ^ 2 := by nlinarith\n                        _ = m ^ 2       := by rw [\u2190 h9]\n                        _ = 2 * n ^ 2   := h2\n        show 2 * k ^ 2 = n ^ 2\n        exact (mul_right_inj' (by norm_num : 2 \u2260 0)).mp h10a\n      have h11 : 2 \u2223 n ^ 2 := by\n        rw [\u2190 h10]\n        -- \u22a2 2 \u2223 2 * k ^ 2\n        exact Nat.dvd_mul_right 2 (k ^ 2)\n      show 2 \u2223 n\n      exact par_si_cuadrado_par h11\n    show 2 \u2223 Nat.gcd m n\n    exact Nat.dvd_gcd h6 h7\n  show False\n  exact h3 h4\n\n-- Lemas usados\n-- ============\n\n-- variable (p k : \u2115)\n-- #check (pow_two n : n ^ 2 = n * n)\n-- #check (Prime.dvd_mul : Nat.Prime p \u2192 (p \u2223 m * n \u2194 p \u2223 m \u2228 p \u2223 n))\n-- #check (prime_two : Nat.Prime 2)\n-- #check (Nat.dvd_gcd : k \u2223 m \u2192 k \u2223 n \u2192 k \u2223 Nat.gcd m n)\n-- #check (Nat.dvd_mul_right m n :  m \u2223 m * n)\n-- #check (mul_right_inj' : k \u2260 0 \u2192 (k * m = k * n \u2194 m = n))\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\/Irracionalidad_de_la_raiz_cuadrada_de_2.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. Las funciones f(x,y) = (x + y)\u00b2 y g(x,y) = x\u00b2 + 2xy + y\u00b2 son iguales<\/h3>\n<p>Demostrar con Lean4 que las funciones &#92;(f(x,y) = (x + y)\u00b2&#92;) y &#92;(g(x,y) = x\u00b2 + 2xy + y&#92;)\u00b2 son iguales.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport  Mathlib.Data.Real.Basic\n\nexample : (fun x y : \u211d \u21a6 (x + y)^2) = (fun x y : \u211d \u21a6 x^2 + 2*x*y + y^2) :=\nby sorry\n<\/pre>\n<pre lang=\"lean\">\nimport  Mathlib.Data.Real.Basic\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (fun x y : \u211d \u21a6 (x + y)^2) = (fun x y : \u211d \u21a6 x^2 + 2*x*y + y^2) :=\nby\n  ext u v\n  -- u v : \u211d\n  -- \u22a2 (u + v) ^ 2 = u ^ 2 + 2 * u * v + v ^ 2\n  ring\n\n-- Comentario: La t\u00e1ctica ext transforma las conclusiones de la forma\n-- (fun x \u21a6 f x) = (fun x \u21a6 g x) en f x = g x.\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (fun x y : \u211d \u21a6 (x + y)^2) = (fun x y : \u211d \u21a6 x^2 + 2*x*y + y^2) :=\nby { ext ; 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\/Demostracion_por_extensionalidad.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 41.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. En \u211d, |a| = |a &#8211; b + b|<\/h3>\n<p>Demostrar con Lean4 que en &#92;(\u211d&#92;), &#92;(|a| = |a &#8211; b + 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 (a b : \u211d)\n\nexample\n  : |a| = |a - b + b| :=\nby sorry\n<\/pre>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (a b : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  : |a| = |a - b + b| :=\nby\n  congr\n  -- a = a - b + b\n  ring\n\n-- Comentario: La t\u00e1ctica congr sustituye una conclusi\u00f3n de la forma\n-- A = B por las igualdades de sus subt\u00e9rminos que no no iguales por\n-- definici\u00f3n. Por ejemplo, sustituye la conclusi\u00f3n (x * f y = g w * f z)\n-- por las conclusiones (x = g w) y (y = z).\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (a b : \u211d)\n  : |a| = |a - b + b| :=\nby { congr ; ring }\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (a b : \u211d)\n  : |a| = |a - b + b| :=\nby ring_nf\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\/Demostracion_por_congruencia.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 41.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. En \u211d, si 1 &lt; a, entonces a &lt; aa<\/h3>\n<p>Demostrar con Lean4 que en &#92;(\u211d&#92;), si &#92;(1 &lt; a&#92;), entonces &#92;(a &lt; aa&#92;)<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {a : \u211d}\n\nexample\n  (h : 1 < a)\n  : a < a * a :=\nby sorry\n<\/pre>\n<p><b>1. Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1n los siguientes lemas<br \/>\n&#92;begin{align}<br \/>\n   &amp;0 &lt; 1                                      &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;(\u2200 a \u2208 \u211d[1a = a]                           &#92;tag{L2} &#92;&#92;<br \/>\n   &amp;(\u2200 a, b, c \u2208 \u211d)[0 &lt; a \u2192 (ba &lt; ca \u2194 b &lt; c)] &#92;tag{L3}<br \/>\n&#92;end{align}<\/p>\n<p>En primer lugar, tenemos que<br \/>\n&#92;[ 0 &lt; a &#92;tag{1} &#92;]<br \/>\nya que<br \/>\n&#92;begin{align}<br \/>\n   0 &amp;&lt; 1    &amp;&amp;&#92;text{[por L1]} &#92;&#92;<br \/>\n     &amp;&lt; a    &amp;&amp;&#92;text{[por la hip\u00f3tesis]}<br \/>\n&#92;end{align}<br \/>\nEntonces,<br \/>\n&#92;begin{align}<br \/>\n   a &amp;= 1a   &amp;&amp;&#92;text{[por L2]} &#92;&#92;<br \/>\n     &amp;&lt; aa   &amp;&amp;&#92;text{[por L3, (1) y la hip\u00f3tesis]}<br \/>\n&#92;end{align}<\/p>\n<p><b>2. Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {a : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : 1 < a)\n  : a < a * a :=\nby\n  have h1 : 0 < a := calc\n    0 < 1 := zero_lt_one\n    _ < a := h\n  show a < a * a\n  calc a = 1 * a := (one_mul a).symm\n       _ < a * a := (mul_lt_mul_right h1).mpr h\n\n-- Comentarios: La t\u00e1ctica (convert e) genera nuevos subojetivos cuya\n-- conclusiones son las diferencias entre el tipo de e y la conclusi\u00f3n.\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : 1 < a)\n  : a < a * a :=\nby\n  convert (mul_lt_mul_right _).2 h\n  . -- \u22a2 a = 1 * a\n    rw [one_mul]\n  . -- \u22a2 0 < a\n    exact lt_trans zero_lt_one h\n\n-- Lemas usados\n-- ============\n\n-- variables (a b c : \u211d)\n-- #check (mul_lt_mul_right : 0 < a \u2192 (b * a < c * a \u2194 b < c))\n-- #check (one_mul a : 1 * a = a)\n-- #check (lt_trans : a < b \u2192 b < c \u2192 a < c)\n-- #check (zero_lt_one : 0 < 1)\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\/???Demostracion_por_conversion.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 41.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. La sucesi\u00f3n constante s\u2099 = c converge a c<\/h3>\n<p>En Lean, una sucesi\u00f3n &#92;(s\u2080, s\u2081, s\u2082, ...&#92;) se puede representar mediante una funci\u00f3n &#92;((s : \u2115 \u2192 \u211d)&#92;) de forma que &#92;(s(n)&#92;) es &#92;(s\u2099&#92;).<\/p>\n<p>Se define que a es el l\u00edmite de la sucesi\u00f3n &#92;(s&#92;), por<\/p>\n<pre lang=\"text\">\ndef limite (s : \u2115 \u2192 \u211d) (a : \u211d) :=\n  \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |s n - a| < \u03b5\n<\/pre>\n<p>Demostrar que el l\u00edmite de la sucesi\u00f3n constante &#92;(s\u2099 = c&#92;) es &#92;(c&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\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 : limite (fun _ : \u2115 \u21a6 c) c :=\nby sorry\n<\/pre>\n<p><b>1. Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Tenemos que demostrar que para cada &#92;(\u03b5 \u2208 \u211d&#92;) tal que &#92;(\u03b5 > 0&#92;), existe un &#92;(N \u2208 \u2115&#92;), tal que &#92;((\u2200n \u2208 \u2115)[n \u2265 N \u2192 |s(n) - a| &lt; \u03b5]&#92;). Basta tomar &#92;(N&#92;) como &#92;(0&#92;), ya que para todo &#92;(n \u2265 N&#92;) se tiene<br \/>\n&#92;begin{align}<br \/>\n   |s(n) - a| &amp;= |a - a| &#92;&#92;<br \/>\n              &amp;= |0|     &#92;&#92;<br \/>\n              &amp;= 0       &#92;&#92;<br \/>\n              &amp;&lt; \u03b5       &#92;&#92;<br \/>\n&#92;end{align}<\/p>\n<p><b>2. Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\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 : limite (fun _ : \u2115 \u21a6 c) 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 _ => c) n - c| < \u03b5\n  use 0\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 0 \u2192 |(fun _ => c) n - c| < \u03b5\n  intros n _hn\n  -- n : \u2115\n  -- hn : n \u2265 0\n  -- \u22a2 |(fun _ => c) n - c| < \u03b5\n  show |(fun _ => c) n - c| < \u03b5\n  calc |(fun _ => c) n - c| = |c - c| := by dsimp\n                          _ = |0|     := by {congr ; exact sub_self c}\n                          _ = 0       := abs_zero\n                          _ < \u03b5       := h\u03b5\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : limite (fun _ : \u2115 \u21a6 c) 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 _ => c) n - c| < \u03b5\n  use 0\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 0 \u2192 |(fun _ => c) n - c| < \u03b5\n  intros n _hn\n  -- n : \u2115\n  -- hn : n \u2265 0\n  -- \u22a2 |(fun _ => c) n - c| < \u03b5\n  show |(fun _ => c) n - c| < \u03b5\n  calc |(fun _ => c) n - c| = 0       := by simp\n                          _ < \u03b5       := h\u03b5\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : limite (fun _ : \u2115 \u21a6 c) 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 _ => c) n - c| < \u03b5\n  aesop\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : limite (fun _ : \u2115 \u21a6 c) 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 _ => c) n - c| < \u03b5\n  aesop\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : limite (fun _ : \u2115 \u21a6 c) c :=\n  fun \u03b5 h\u03b5 \u21a6 by aesop\n\n-- Lemas usados\n-- ============\n\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\/Convergencia_de_la_sucesion_constante.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>3. Demostraciones con Isabelle\/HOL<\/b><\/p>\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><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 41.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. La ra\u00edz cuadrada de 2 es irracional 2. Las funciones f(x,y) = (x + y)\u00b2 y g(x,y) = x\u00b2 + 2xy + y\u00b2 son iguales 3. En \u211d, |a| = |a &#8211; b + b| 4. En \u211d, si 1&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[335],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8098"}],"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=8098"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8098\/revisions"}],"predecessor-version":[{"id":8100,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8098\/revisions\/8100"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8098"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8098"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8098"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}