Demostrar con Lean4 que el l\u00edmite de \(u\u2099\) es \(a\) si, y s\u00f3lo si, el de \(u\u2099-a\) es \(0\).<\/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}\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<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Se prueba por la siguiente cadena de equivalencias
\n\begin{align}
\n &\text{el l\u00edmite de \(u\u2099\) es \(a\)} \\
\n &\u2194 (\u2200\u03b5>0)(\u2203N)(\u2200n\u2265N)[|u(n) - a| < \u03b5] \\
\n &\u2194 (\u2200\u03b5>0)(\u2203N)(\u2200n\u2265N)[|(u(n) - a) - 0| < \u03b5] \\
\n &\u2194 \text{el l\u00edmite de \(u\u2099-a\) es \(0\)}
\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}\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