ForMatUS: Pruebas en Lean de la unicidad del límite de las sucesiones

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan pruebas en Lean de la unicidad del límite de las sucesiones.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

Pruebas en Lean de “Si |x – y| ≤ ε, para todo ε > 0, entonces x = y”

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan pruebas en Lean de la propiedad:

Si |x – y| ≤ ε, para todo ε > 0, entonces x = y

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada