En Lean, una sucesi\u00f3n \(u\u2080, u\u2081, u\u2082, …\) se puede representar mediante una funci\u00f3n \((u : \u2115 \u2192 \u211d)\) de forma que \(u(n)\) es \(u\u2099\).<\/p>\n
Se define que \(a\) es el l\u00edmite de la sucesi\u00f3n \(u\), por<\/p>\n
\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>\nDemostrar con Lean4 que cada sucesi\u00f3n tiene como m\u00e1ximo un l\u00edmite.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\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>\n1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Tenemos que demostrar que si \(u\) es una sucesi\u00f3n y \(a\) y \(b\) son l\u00edmites de \(u\), entonces \(a = b\). Para ello, basta demostrar que \(a \u2264 b\) y \(b \u2264 a\).<\/p>\n
Demostraremos que \(b \u2264 a\) por reducci\u00f3n al absurdo. Supongamos que \(b \u2270 a\). Sea \(\u03b5 = b - a\). Entonces, \u03b5\/2 > 0 y, puesto que \(a\) es un l\u00edmite de \(u\), existe un \(A \u2208 \u2115\) tal que
\n\[ (\u2200n \u2208 \u2115)\left[n \u2265 A \u2192 |u(n) - a| < \frac{\u03b5}{2}\right] \tag{1} \]
\ny, puesto que \(b\) tambi\u00e9n es un l\u00edmite de \(u\), existe un \(B \u2208 \u2115\) tal que
\n\[ (\u2200n \u2208 \u2115)\left[n \u2265 B \u2192 |u(n) - b| < \frac{\u03b5}{2}\right] \tag{2} \]
\nSea \(N = m\u00e1x(A, B)\). Entonces, \(N \u2265 A\) y \(N \u2265 B\) y, por (2) y (3), se tiene
\n\begin{align}
\n |u(N) - a| &< \frac{\u03b5}{2} \tag{3} \\
\n |u(N) - b| &< \frac{\u03b5}{2} \tag{4}
\n\end{align}
\nPara obtener una contradicci\u00f3n basta probar que \(\u03b5 < \u03b5\). Su prueba es
\n\begin{align}
\n \u03b5 &= b - a \\
\n &= |b - a| \\
\n &= |(b - a) + (u(N) - u(N))| \\
\n &= |(u(N) - a) + (b - u(N))| \\
\n &\u2264 |u(N) - a| + |b - u(N)| \\
\n &= |u(N) - a| + |u(N) - b| \\
\n &< \frac{\u03b5}{2} + \frac{\u03b5}{2} && \text{[por (3) y (4)]} \\
\n &= \u03b5
\n\end{align}<\/p>\n
La demostraci\u00f3n de \(a \u2264 b\) es an\u00e1loga a la anterior.<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\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>\nDemostraciones interactivas<\/h3>\n