Demostrar con Lean4 que 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\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\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<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(\u03b5 \u2208 \u211d\) tal que \(\u03b5 > 0\). Tenemos que demostrar que
\n\[ (\u2203 N)(\u2200 n \u2265 N)[|(u(n) + c) - (a + c)| < \u03b5] \tag{1} \]
\nPuesto que el l\u00edmite de la sucesi\u00f3n \(u\) es \(a\), existe un \(k\) tal que
\n\[ (\u2200 n \u2265 k)[|u(n) - a| < \u03b5] \tag{2} \]
\nVeamos que con k se verifica (1); es decir, que
\n\[ (\u2200 n \u2265 k)[|(u(n) + c) - (a + c)| < \u03b5] \]
\nSea \(n \u2265 k\). Entonces, por (2),
\n\[ |u(n) - a| < \u03b5 \tag{3} \]
\ny, por consiguiente,
\n\begin{align}
\n |(u(n) + c) - (a + c)| &= |u(n) - a| \\
\n &< \u03b5 &&\text{[por (3)]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\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