Las sucesiones divergentes positivas no tienen límites finitos

En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.

Se define que a es el límite de la sucesión u, por

donde se usa la notación |x| para el valor absoluto de x

La sucesión u diverge positivamente cuando, para cada número real A, se puede encontrar un número natural m tal que, para n > m , se tenga u(n) > A. En Lean se puede definir por

Demostrar que si u diverge positivamente, entonces ningún número real es límite de u.

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Si a es un punto de acumulación de la sucesión de Cauchy u, entonces a es el límite de u

En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.

Para extraer una subsucesión se aplica una función de extracción queconserva el orden; por ejemplo, la subsucesión

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

que a es un límite de u por

que a es un punto de acumulación de u por

que la sucesión u es de Cauchy por

Demostrar que si u es una sucesión de Cauchy y a es un punto de acumulación de u, entonces a es el límite de u.

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

El punto de acumulación de las sucesiones convergente es su límite

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

que a es un límite de u por

que u es convergente por

que a es un punto de acumulación de u por

Demostrar que si u es una sucesión convergente y a es un punto de acumulación de u, entonces a es un límite de u.

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las subsucesiones tienen el mismo límite que la sucesión

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

que v es una subsucesión de u por

y que a es un límite de u por

Demostrar que las subsucesiones de una sucesión convergente tienen el mismo límite que la sucesión.

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Si a es un punto de acumulación de u, entonces ∀ε>0, ∀ N, ∃k≥N, |u(k)−a| < ε

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

También se puede definir que a es un límite de u por

Los puntos de acumulación de una sucesión son los límites de sus subsucesiones. En Lean se puede definir por

Demostrar que si a es un punto de acumulación de u, entonces

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]