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 \(cu\u2099\) es \(ca\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable (u v : \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 n \u21a6 c * (u n)) (c * a) :=\nby\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 \u2208 \u2115)(\u2200 n \u2265 N)[|cu\u2099 - ca| < \u03b5] \tag{1}\]
\nDistinguiremos dos casos seg\u00fan sea \(c = 0\) o no.<\/p>\n
Primer caso: Supongamos que \(c = 0\). Entonces, (1) se reduce a
\n\[ (\u2203 N \u2208 \u2115)(\u2200 n \u2265 N)[|0\u00b7u\u2099 - 0\u00b7a| < \u03b5] \]
\nes decir,
\n\[ (\u2203 N \u2208 \u2115)(\u2200 n \u2265 N)[0 < \u03b5] \]
\nque se verifica para cualquier n\u00famero \(N\), ya que \(\u03b5 > 0\).<\/p>\n
Segundo caso: Supongamos que \(c \u2260 0\). Entonces, \(\dfrac{\u03b5}{|c|}\) > 0 y, puesto que el l\u00edmite de \(u\u2099\) es \(a\), existe un \(k \u2208 \u2115\) tal que
\n\[ (\u2200 n \u2265 k)[|u\u2099 - a| < \frac{\u03b5}{|c|}] \tag{2} \]
\nVeamos que con \(k\) se cumple (1). En efecto, sea \(n \u2265 k\). Entonces,
\n\begin{align}
\n |cu\u2099 - ca| &= |c(u\u2099 - a)| \\
\n &= |c||u\u2099 - a| \\
\n &< |c|\frac{\u03b5}{|c|} &&\text{[por (2)]} \\
\n &= \u03b5
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable (u v : \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 n \u21a6 c * (u n)) (c * a) :=\nby\n by_cases hc : c = 0\n . -- hc : c = 0\n subst hc\n -- \u22a2 limite (fun n => 0 * u n) (0 * a)\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 n => 0 * u n) n - 0 * a| < \u03b5\n aesop\n . -- hc : \u00acc = 0\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 n => c * u n) n - c * a| < \u03b5\n have hc' : 0 < |c| := abs_pos.mpr hc\n have h\u03b5c : 0 < \u03b5 \/ |c| := div_pos h\u03b5 hc'\n specialize h (\u03b5\/|c|) h\u03b5c\n -- h : \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |u n - a| < \u03b5 \/ |c|\n cases' h with N hN\n -- N : \u2115\n -- hN : \u2200 (n : \u2115), n \u2265 N \u2192 |u n - a| < \u03b5 \/ |c|\n use N\n -- \u22a2 \u2200 (n : \u2115), n \u2265 N \u2192 |(fun n => c * u n) n - c * a| < \u03b5\n intros n hn\n -- n : \u2115\n -- hn : n \u2265 N\n -- \u22a2 |(fun n => c * u n) n - c * a| < \u03b5\n specialize hN n hn\n -- hN : |u n - a| < \u03b5 \/ |c|\n dsimp only\n calc |c * u n - c * a|\n = |c * (u n - a)| := congr_arg abs (mul_sub c (u n) a).symm\n _ = |c| * |u n - a| := abs_mul c (u n - a)\n _ < |c| * (\u03b5 \/ |c|) := (mul_lt_mul_left hc').mpr hN\n _ = \u03b5 := mul_div_cancel' \u03b5 (ne_of_gt hc')\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : limite u a)\n : limite (fun n \u21a6 c * (u n)) (c * a) :=\nby\n by_cases hc : c = 0\n . -- hc : c = 0\n subst hc\n -- \u22a2 limite (fun n => 0 * u n) (0 * a)\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 n => 0 * u n) n - 0 * a| < \u03b5\n aesop\n . -- hc : \u00acc = 0\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 n => c * u n) n - c * a| < \u03b5\n have hc' : 0 < |c| := abs_pos.mpr hc\n have h\u03b5c : 0 < \u03b5 \/ |c| := div_pos h\u03b5 hc'\n specialize h (\u03b5\/|c|) h\u03b5c\n -- h : \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |u n - a| < \u03b5 \/ |c|\n cases' h with N hN\n -- N : \u2115\n -- hN : \u2200 (n : \u2115), n \u2265 N \u2192 |u n - a| < \u03b5 \/ |c|\n use N\n -- \u22a2 \u2200 (n : \u2115), n \u2265 N \u2192 |(fun n => c * u n) n - c * a| < \u03b5\n intros n hn\n -- n : \u2115\n -- hn : n \u2265 N\n -- \u22a2 |(fun n => c * u n) n - c * a| < \u03b5\n specialize hN n hn\n -- hN : |u n - a| < \u03b5 \/ |c|\n dsimp only\n -- \u22a2 |c * u n - c * a| < \u03b5\n rw [\u2190 mul_sub]\n -- \u22a2 |c * (u n - a)| < \u03b5\n rw [abs_mul]\n -- \u22a2 |c| * |u n - a| < \u03b5\n rw [\u2190 lt_div_iff' hc']\n -- \u22a2 |u n - a| < \u03b5 \/ |c|\n exact hN\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : limite u a)\n : limite (fun n \u21a6 c * (u n)) (c * a) :=\nby\n by_cases hc : c = 0\n . subst hc\n intros \u03b5 h\u03b5\n aesop\n . intros \u03b5 h\u03b5\n have hc' : 0 < |c| := by aesop\n have h\u03b5c : 0 < \u03b5 \/ |c| := div_pos h\u03b5 hc'\n cases' h (\u03b5\/|c|) h\u03b5c with N hN\n use N\n intros n hn\n specialize hN n hn\n dsimp only\n rw [\u2190 mul_sub, abs_mul, \u2190 lt_div_iff' hc']\n exact hN\n\n-- Lemas usados\n-- ============\n\n-- variable (b c : \u211d)\n-- #check (abs_mul a b : |a * b| = |a| * |b|)\n-- #check (abs_pos.mpr : a \u2260 0 \u2192 0 < |a|)\n-- #check (div_pos : 0 < a \u2192 0 < b \u2192 0 < a \/ b)\n-- #check (lt_div_iff' : 0 < c \u2192 (a < b \/ c \u2194 c * a < b))\n-- #check (mul_div_cancel' a : b \u2260 0 \u2192 b * (a \/ b) = a)\n-- #check (mul_lt_mul_left : 0 < a \u2192 (a * b < a * c \u2194 b < c))\n-- #check (mul_sub a b c : a * (b - c) = a * b - a * c)\n<\/pre>\n