En Lean4, una sucesi\u00f3n \(u_0, u_1, u_2, \dots\) se puede representar mediante una funci\u00f3n \(u : \u2115 \u2192 \u211d\) de forma que \(u(n)\) es el \(n\)-\u00e9simo t\u00e9rmino de la sucesi\u00f3n.<\/p>\n
Se define que \(a\) l\u00edmite de la sucesi\u00f3n \(u\) como sigue<\/p>\n
\n def limite (u : \u2115 \u2192 \u211d) (c : \u211d) :=\n \u2200 \u03b5 > 0, \u2203 k, \u2200 n \u2265 k, |u n - c| < \u03b5\n<\/pre>\nDemostrar que si \((\u2200 n)[u_n \u2264 v_n]\), \(a\) es l\u00edmite de \(u_n\) y \(c\) es l\u00edmite de \(v_n\), entonces \(a \u2264 c\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\n\nvariable (u v : \u2115 \u2192 \u211d)\nvariable (a c : \u211d)\n\ndef limite (u : \u2115 \u2192 \u211d) (c : \u211d) :=\n \u2200 \u03b5 > 0, \u2203 k, \u2200 n \u2265 k, |u n - c| < \u03b5\n\nexample\n (hu : limite u a)\n (hv : limite v c)\n (huv : \u2200 n, u n \u2264 v n)\n : a \u2264 c :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Por reduccion al absurdo. Supongamos que \(a \u2270 c\). Entonces,
\n\[ c < a \tag{1} \]
\nSea
\n\[ \u03b5 = \frac{a - c}{2} \tag{2} \]
\nPor (1),
\n\[ \u03b5 > 0 \]
\nPor tanto, puesto que \(a\) es l\u00edmite de \(u_n\), existe un \(p \u2208 \u2115\) tal que
\n\[ (\u2200 n)[n \u2265 p \u2192 |u_n - a| < \u03b5] \tag{3} \]
\nAn\u00e1logamente, puesto que c es l\u00edmite de \(v_n\), existe un \(q \u2208 \u2115\) tal que
\n\[ (\u2200 n)[n \u2265 q \u2192 |v_n - c| < \u03b5] \tag{4} \]
\nSea
\n\[ k = \max(p, q) \]
\nEntonces, \(k \u2265 p\) y, por (3),
\n\[ |u_k - a| < \u03b5 \tag{5} \]
\nAn\u00e1logamente, \(k \u2265 q\) y, por (4),
\n\[ |v_k - c| < \u03b5 \tag{6} \]
\nAdem\u00e1s, por la hip\u00f3tesis,
\n\[ u_k \u2264 v_k \tag{7} \]
\nPor tanto,
\n\begin{align}
\n a - c &= (a - u_k) + (u_k - c) \\
\n &\u2264 (a - u_k) + (v_k - c) &&\text{[por (7)]} \\
\n &\u2264 |(a - u_k) + (v_k - c)| \\
\n &\u2264 |a - u_k| + |v_k - c| \\
\n &= |u_k - a| + |v_k - c| \\
\n &< \u03b5 + \u03b5 &&\text{[por (5) y (6)]} \\
\n &= a - c &&\text{[por (2)]}
\n\end{align}
\nLuego,
\n\[ a - c < a - c \]
\nque es una contradicci\u00f3n.<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Real.Basic\n\nvariable (u v : \u2115 \u2192 \u211d)\nvariable (a c : \u211d)\n\ndef limite (u : \u2115 \u2192 \u211d) (c : \u211d) :=\n \u2200 \u03b5 > 0, \u2203 k, \u2200 n \u2265 k, |u n - c| < \u03b5\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u a)\n (hv : limite v c)\n (huv : \u2200 n, u n \u2264 v n)\n : a \u2264 c :=\nby\n by_contra h\n -- h : \u00aca \u2264 c\n -- \u22a2 False\n have hca : c < a := not_le.mp h\n set \u03b5 := (a - c) \/2\n have h\u03b5 : 0 < \u03b5 := half_pos (sub_pos.mpr hca)\n obtain \u27e8ku, hku : \u2200 n, n \u2265 ku \u2192 |u n - a| < \u03b5\u27e9 := hu \u03b5 h\u03b5\n obtain \u27e8kv, hkv : \u2200 n, n \u2265 kv \u2192 |v n - c| < \u03b5\u27e9 := hv \u03b5 h\u03b5\n let k := max ku kv\n have hku' : ku \u2264 k := le_max_left ku kv\n have hkv' : kv \u2264 k := le_max_right ku kv\n have ha : |u k - a| < \u03b5 := hku k hku'\n have hc : |v k - c| < \u03b5 := hkv k hkv'\n have hk : u k - c \u2264 v k - c := sub_le_sub_right (huv k) c\n have hac1 : a - c < a - c := by\n calc a - c\n = (a - u k) + (u k - c) := by ring\n _ \u2264 (a - u k) + (v k - c) := add_le_add_left hk (a - u k)\n _ \u2264 |(a - u k) + (v k - c)| := le_abs_self ((a - u k) + (v k - c))\n _ \u2264 |a - u k| + |v k - c| := abs_add (a - u k) (v k - c)\n _ = |u k - a| + |v k - c| := by simp only [abs_sub_comm]\n _ < \u03b5 + \u03b5 := add_lt_add ha hc\n _ = a - c := add_halves (a - c)\n have hac2 : \u00ac a - c < a -c := lt_irrefl (a - c)\n show False\n exact hac2 hac1\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u a)\n (hv : limite v c)\n (huv : \u2200 n, u n \u2264 v n)\n : a \u2264 c :=\nby\n by_contra h\n -- h : \u00aca \u2264 c\n -- \u22a2 False\n have hca : c < a := not_le.mp h\n set \u03b5 := (a - c) \/2 with h\u03b5\n obtain \u27e8ku, hku : \u2200 n, n \u2265 ku \u2192 |u n - a| < \u03b5\u27e9 := hu \u03b5 (by linarith)\n obtain \u27e8kv, hkv : \u2200 n, n \u2265 kv \u2192 |v n - c| < \u03b5\u27e9 := hv \u03b5 (by linarith)\n let k := max ku kv\n have ha : |u k - a| < \u03b5 := hku k (le_max_left ku kv)\n have hc : |v k - c| < \u03b5 := hkv k (le_max_right ku kv)\n have hk : u k - c \u2264 v k - c := sub_le_sub_right (huv k) c\n have hac1 : a - c < a -c := by\n calc a - c\n = (a - u k) + (u k - c) := by ring\n _ \u2264 (a - u k) + (v k - c) := add_le_add_left hk (a - u k)\n _ \u2264 |(a - u k) + (v k - c)| := le_abs_self ((a - u k) + (v k - c))\n _ \u2264 |a - u k| + |v k - c| := abs_add (a - u k) (v k - c)\n _ = |u k - a| + |v k - c| := by simp only [abs_sub_comm]\n _ < \u03b5 + \u03b5 := add_lt_add ha hc\n _ = a - c := add_halves (a - c)\n have hac2 : \u00ac a - c < a -c := lt_irrefl (a - c)\n show False\n exact hac2 hac1\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u a)\n (hv : limite v c)\n (huv : \u2200 n, u n \u2264 v n)\n : a \u2264 c :=\nby\n by_contra h\n -- h : \u00aca \u2264 c\n -- \u22a2 False\n have hca : c < a := not_le.mp h\n set \u03b5 := (a - c) \/2 with h\u03b5\n obtain \u27e8ku, hku : \u2200 n, n \u2265 ku \u2192 |u n - a| < \u03b5\u27e9 := hu \u03b5 (by linarith)\n obtain \u27e8kv, hkv : \u2200 n, n \u2265 kv \u2192 |v n - c| < \u03b5\u27e9 := hv \u03b5 (by linarith)\n let k := max ku kv\n have ha : |u k - a| < \u03b5 := hku k (le_max_left ku kv)\n have hc : |v k - c| < \u03b5 := hkv k (le_max_right ku kv)\n have hk : u k - c \u2264 v k - c := sub_le_sub_right (huv k) c\n have hac1 : a - c < a -c := by\n calc a - c\n = (a - u k) + (u k - c) := by ring\n _ \u2264 (a - u k) + (v k - c) := add_le_add_left hk (a - u k)\n _ \u2264 |(a - u k) + (v k - c)| := by simp [le_abs_self]\n _ \u2264 |a - u k| + |v k - c| := by simp [abs_add]\n _ = |u k - a| + |v k - c| := by simp [abs_sub_comm]\n _ < \u03b5 + \u03b5 := add_lt_add ha hc\n _ = a - c := by simp\n have hac2 : \u00ac a - c < a -c := lt_irrefl (a - c)\n show False\n exact hac2 hac1\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u a)\n (hv : limite v c)\n (huv : \u2200 n, u n \u2264 v n)\n : a \u2264 c :=\nby\n apply le_of_not_lt\n -- \u22a2 \u00acc < a\n intro hca\n -- hca : c < a\n -- \u22a2 False\n set \u03b5 := (a - c) \/2 with h\u03b5\n cases' hu \u03b5 (by linarith) with ku hku\n -- ku : \u2115\n -- hku : \u2200 (n : \u2115), n \u2265 ku \u2192 |u n - a| < \u03b5\n cases' hv \u03b5 (by linarith) with kv hkv\n -- kv : \u2115\n -- hkv : \u2200 (n : \u2115), n \u2265 kv \u2192 |v n - c| < \u03b5\n let k := max ku kv\n have ha : |u k - a| < \u03b5 := hku k (le_max_left ku kv)\n have hc : |v k - c| < \u03b5 := hkv k (le_max_right ku kv)\n have hk : u k \u2264 v k := huv k\n apply lt_irrefl (a - c)\n -- \u22a2 a - c < a - c\n rw [abs_lt] at ha hc\n -- ha : -\u03b5 < u k - a \u2227 u k - a < \u03b5\n -- hc : -\u03b5 < v k - c \u2227 v k - c < \u03b5\n linarith\n\n-- Lemas usados\n-- ============\n\n-- variable (b d : \u211d)\n-- #check (abs_add a b : |a + b| \u2264 |a| + |b|)\n-- #check (abs_lt: |a| < b \u2194 -b < a \u2227 a < b)\n-- #check (abs_sub_comm a b : |a - b| = |b - a|)\n-- #check (add_halves a : a \/ 2 + a \/ 2 = a)\n-- #check (add_le_add_left : b \u2264 c \u2192 \u2200 a, a + b \u2264 a + c)\n-- #check (add_lt_add : a < b \u2192 c < d \u2192 a + c < b + d)\n-- #check (half_pos : 0 < a \u2192 0 < a \/ 2)\n-- #check (le_abs_self a : a \u2264 |a|)\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 (le_of_not_lt : \u00acb < a \u2192 a \u2264 b)\n-- #check (lt_irrefl a : \u00aca < a)\n-- #check (not_le : \u00aca \u2264 b \u2194 b < a)\n-- #check (sub_le_sub_right : a \u2264 b \u2192 \u2200 c, a - c \u2264 b - c)\n-- #check (sub_pos : 0 < a - b \u2194 b < a)\n<\/pre>\n