Límite de sucesiones no decrecientes

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

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

y que la sucesión u es no decreciente por

Demostrar que si u es una sucesión no decreciente y su límite es a, entonces u(n) ≤ a para todo 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]

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]

Las particiones definen relaciones reflexivas

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

Una familia de subconjuntos de X es una partición de X si cada elemento de X pertenece a un único conjunto de P y todos los elementos de P son no vacíos. Se puede definir en Lean por

Demostrar que si P es una partición de X, entonces la relación definida por P es reflexiva.

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 clases de equivalencia de elementos no relacionados son disjuntas

Demostrar que las clases de equivalencia de elementos no relacionados son disjuntas.

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]