Demostrar con Lean4 que si \(u_n\) es una sucesi\u00f3n convergente, entonces est\u00e1 acotada; es decir,
\n\[ (\u2203 k \u2208 \u2115)(\u2203 b \u2208 \u211d)(\u2200 n \u2208 \u2115)[n \u2265 k \u2192 |u_n| \u2264 b] \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable {u : \u2115 \u2192 \u211d}\n\n-- (limite u c) expresa que el l\u00edmite de u es c.\ndef limite (u : \u2115 \u2192 \u211d) (c : \u211d) :=\n \u2200 \u03b5 > 0, \u2203 k, \u2200 n \u2265 k, |u n - c| \u2264 \u03b5\n\n-- (convergente u) expresa que u es convergente.\ndef convergente (u : \u2115 \u2192 \u211d) :=\n \u2203 a, limite u a\n\nexample\n (h : convergente u)\n : \u2203 k b, \u2200 n, n \u2265 k \u2192 |u n| \u2264 b :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Puesto que la sucesi\u00f3n \(u_n\) es convergente, existe un \(a \u2208 \u211d\) tal que
\n\[ \lim(u_n) = a \]
\nLuego, existe un \(k \u2208 \u2115\) tal que
\n\[ (\u2200 n \u2208 \u2115)[n \u2265 k \u2192 |u_n – a | < 1] \tag{1} \]
\nVeamos que
\n\[ (\u2200 n \u2208 \u2115)[n \u2265 k \u2192 |u_n| \u2264 1 + |a]] \]
\nPara ello, sea \(n \u2208 \u2115\) tal que
\n\[ n \u2265 k \tag{2} \]
\nEntonces,
\n\begin{align}
\n |u_n| &= |u_n – a + a| \\
\n &\u2264 |u_n – a| + |a| \\
\n &\u2264 1 + |a| &&\text{[por (1) y (2)]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable {u : \u2115 \u2192 \u211d}\n\n-- (limite u c) expresa que el l\u00edmite de u es c.\ndef limite (u : \u2115 \u2192 \u211d) (c : \u211d) :=\n \u2200 \u03b5 > 0, \u2203 k, \u2200 n \u2265 k, |u n - c| \u2264 \u03b5\n\n-- (convergente u) expresa que u es convergente.\ndef convergente (u : \u2115 \u2192 \u211d) :=\n \u2203 a, limite u a\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : convergente u)\n : \u2203 k b, \u2200 n, n \u2265 k \u2192 |u n| \u2264 b :=\nby\n cases' h with a ua\n -- a : \u211d\n -- ua : limite u a\n cases' ua 1 zero_lt_one with k h\n -- k : \u2115\n -- h : \u2200 (n : \u2115), n \u2265 k \u2192 |u n - a| \u2264 1\n use k, 1 + |a|\n -- \u22a2 \u2200 (n : \u2115), n \u2265 k \u2192 |u n| \u2264 1 + |a|\n intros n hn\n -- n : \u2115\n -- hn : n \u2265 k\n -- \u22a2 |u n| \u2264 1 + |a|\n specialize h n hn\n -- \u22a2 |u n| \u2264 1 + |a|\n calc |u n|\n = |u n - a + a| := congr_arg abs (eq_add_of_sub_eq rfl)\n _ \u2264 |u n - a| + |a| := abs_add (u n - a) a\n _ \u2264 1 + |a| := add_le_add_right h |a|\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : convergente u)\n : \u2203 k b, \u2200 n, n \u2265 k \u2192 |u n| \u2264 b :=\nby\n cases' h with a ua\n -- a : \u211d\n -- ua : limite u a\n cases' ua 1 zero_lt_one with k h\n -- k : \u2115\n -- h : \u2200 (n : \u2115), n \u2265 k \u2192 |u n - a| \u2264 1\n use k, 1 + |a|\n -- \u22a2 \u2200 (n : \u2115), n \u2265 k \u2192 |u n| \u2264 1 + |a|\n intros n hn\n -- n : \u2115\n -- hn : n \u2265 k\n -- \u22a2 |u n| \u2264 1 + |a|\n specialize h n hn\n -- h : |u n - a| \u2264 1\n calc |u n|\n = |u n - a + a| := by ring_nf\n _ \u2264 |u n - a| + |a| := abs_add (u n - a) a\n _ \u2264 1 + |a| := by linarith\n\n-- Lemas usados\n-- ============\n\n-- variable (a b c : \u211d)\n-- #check (abs_add a b : |a + b| \u2264 |a| + |b|)\n-- #check (add_le_add_right : b \u2264 c \u2192 \u2200 a, b + a \u2264 c + a)\n-- #check (eq_add_of_sub_eq : a - c = b \u2192 a = b + c)\n-- #check (zero_lt_one : 0 < 1)\n<\/pre>\n