Demostrar con Lean4 el teorema del emparedado.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\n\nvariable (u v w : \u2115 \u2192 \u211d)\nvariable (a : \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| \u2264 \u03b5\n\nexample\n (hu : limite u a)\n (hw : limite w a)\n (h1 : \u2200 n, u n \u2264 v n)\n (h2 : \u2200 n, v n \u2264 w n) :\n limite v a :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Tenemos que demostrar que para cada \(\u03b5 > 0\), existe un \(N \u2208 \u2115\) tal que
\n\[ (\u2200 n \u2265 N)[|v(n) – a| \u2264 \u03b5] \tag{1} \]<\/p>\n
Puesto que el l\u00edmite de \(u\) es \(a\), existe un \(U \u2208 \u2115\) tal que
\n\[ (\u2200 n \u2265 U)[|u(n) – a| \u2264 \u03b5] \tag{2} \]
\ny, puesto que el l\u00edmite de \(w\) es \(a\), existe un \(W \u2208 \u2115\) tal que
\n\[ (\u2200 n \u2265 W)[|w(n) – a| \u2264 \u03b5] \tag{3} \]
\nSea \(N = \text{m\u00e1x}(U, W)\). Veamos que se verifica (1). Para ello, sea \(n \u2265 N\). Entonces, \(n \u2265 U\), \(n \u2265 W\) y, por (2) y (3), se tiene que
\n\begin{align}
\n |u(n) – a| &\u2264 \u03b5 \tag{4} \\
\n |w(n) – a| &\u2264 \u03b5 \tag{5}
\n\end{align}
\nPara demostrar que
\n\[ |v(n) – a| \u2264 \u03b5 \]
\nbasta demostrar las siguientes desigualdades
\n\begin{align}
\n -\u03b5 \u2264 &v(n) – a \tag{6} \\
\n &v(n) – a \u2264 \u03b5 \tag{7}
\n\end{align}
\nLa demostraci\u00f3n de (6) es
\n\begin{align}
\n -\u03b5 &\u2264 u(n) – a &&\text{[por (4)]} \\
\n &\u2264 v(n) – a &&\text{[por hip\u00f3tesis]}
\n\end{align}
\nLa demostraci\u00f3n de (7) es
\n\begin{align}
\n v(n) – a &\u2264 w(n) – a &&\text{[por hip\u00f3tesis]} \\
\n &\u2264 \u03b5 &&\text{[por (5)]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Real.Basic\n\nvariable (u v w : \u2115 \u2192 \u211d)\nvariable (a : \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| \u2264 \u03b5\n\n-- Nota. En la demostraci\u00f3n se usar\u00e1 el siguiente lema:\nlemma max_ge_iff\n {p q r : \u2115}\n : r \u2265 max p q \u2194 r \u2265 p \u2227 r \u2265 q :=\n max_le_iff\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u a)\n (hw : limite w a)\n (h1 : \u2200 n, u n \u2264 v n)\n (h2 : \u2200 n, v n \u2264 w n) :\n limite v a :=\nby\n intros \u03b5 h\u03b5\n -- \u03b5 : \u211d\n -- h\u03b5 : \u03b5 > 0\n -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |v n - a| \u2264 \u03b5\n rcases hu \u03b5 h\u03b5 with \u27e8U, hU\u27e9\n -- U : \u2115\n -- hU : \u2200 (n : \u2115), n \u2265 U \u2192 |u n - a| \u2264 \u03b5\n clear hu\n rcases hw \u03b5 h\u03b5 with \u27e8W, hW\u27e9\n -- W : \u2115\n -- hW : \u2200 (n : \u2115), n \u2265 W \u2192 |w n - a| \u2264 \u03b5\n clear hw h\u03b5\n use max U W\n intros n hn\n -- n : \u2115\n -- hn : n \u2265 max U W\n -- \u22a2 |v n - a| \u2264 \u03b5\n rw [max_ge_iff] at hn\n -- hn : n \u2265 U \u2227 n \u2265 W\n specialize hU n hn.1\n -- hU : |u n - a| \u2264 \u03b5\n specialize hW n hn.2\n -- hW : |w n - a| \u2264 \u03b5\n specialize h1 n\n -- h1 : u n \u2264 v n\n specialize h2 n\n -- h2 : v n \u2264 w n\n clear hn\n rw [abs_le] at *\n -- \u22a2 -\u03b5 \u2264 v n - a \u2227 v n - a \u2264 \u03b5\n constructor\n . -- \u22a2 -\u03b5 \u2264 v n - a\n calc -\u03b5\n \u2264 u n - a := hU.1\n _ \u2264 v n - a := by linarith\n . -- \u22a2 v n - a \u2264 \u03b5\n calc v n - a\n \u2264 w n - a := by linarith\n _ \u2264 \u03b5 := hW.2\n\n-- 2\u00aa demostraci\u00f3n\nexample\n (hu : limite u a)\n (hw : limite w a)\n (h1 : \u2200 n, u n \u2264 v n)\n (h2 : \u2200 n, v n \u2264 w n) :\n limite v a :=\nby\n intros \u03b5 h\u03b5\n -- \u03b5 : \u211d\n -- h\u03b5 : \u03b5 > 0\n -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |v n - a| \u2264 \u03b5\n rcases hu \u03b5 h\u03b5 with \u27e8U, hU\u27e9\n -- U : \u2115\n -- hU : \u2200 (n : \u2115), n \u2265 U \u2192 |u n - a| \u2264 \u03b5\n clear hu\n rcases hw \u03b5 h\u03b5 with \u27e8W, hW\u27e9\n -- W : \u2115\n -- hW : \u2200 (n : \u2115), n \u2265 W \u2192 |w n - a| \u2264 \u03b5\n clear hw h\u03b5\n use max U W\n intros n hn\n -- n : \u2115\n -- hn : n \u2265 max U W\n rw [max_ge_iff] at hn\n -- hn : n \u2265 U \u2227 n \u2265 W\n specialize hU n (by linarith)\n -- hU : |u n - a| \u2264 \u03b5\n specialize hW n (by linarith)\n -- hW : |w n - a| \u2264 \u03b5\n specialize h1 n\n -- h1 : u n \u2264 v n\n specialize h2 n\n -- h2 : v n \u2264 w n\n rw [abs_le] at *\n -- \u22a2 -\u03b5 \u2264 v n - a \u2227 v n - a \u2264 \u03b5\n constructor\n . -- \u22a2 -\u03b5 \u2264 v n - a\n linarith\n . -- \u22a2 v n - a \u2264 \u03b5\n linarith\n\n-- 3\u00aa demostraci\u00f3n\nexample\n (hu : limite u a)\n (hw : limite w a)\n (h1 : \u2200 n, u n \u2264 v n)\n (h2 : \u2200 n, v n \u2264 w n) :\n limite v a :=\nby\n intros \u03b5 h\u03b5\n -- \u03b5 : \u211d\n -- h\u03b5 : \u03b5 > 0\n -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |v n - a| \u2264 \u03b5\n rcases hu \u03b5 h\u03b5 with \u27e8U, hU\u27e9\n -- U : \u2115\n -- hU : \u2200 (n : \u2115), n \u2265 U \u2192 |u n - a| \u2264 \u03b5\n clear hu\n rcases hw \u03b5 h\u03b5 with \u27e8W, hW\u27e9\n -- W : \u2115\n -- hW : \u2200 (n : \u2115), n \u2265 W \u2192 |w n - a| \u2264 \u03b5\n clear hw h\u03b5\n use max U W\n intros n hn\n -- n : \u2115\n -- hn : n \u2265 max U W\n -- \u22a2 |v n - a| \u2264 \u03b5\n rw [max_ge_iff] at hn\n -- hn : n \u2265 U \u2227 n \u2265 W\n specialize hU n (by linarith)\n -- hU : |u n - a| \u2264 \u03b5\n specialize hW n (by linarith)\n -- hW : |w n - a| \u2264 \u03b5\n specialize h1 n\n -- h1 : u n \u2264 v n\n specialize h2 n\n -- h2 : v n \u2264 w n\n rw [abs_le] at *\n -- hU : -\u03b5 \u2264 u n - a \u2227 u n - a \u2264 \u03b5\n -- hW : -\u03b5 \u2264 w n - a \u2227 w n - a \u2264 \u03b5\n -- \u22a2 -\u03b5 \u2264 v n - a \u2227 v n - a \u2264 \u03b5\n constructor <;> linarith\n<\/pre>\n