ForMatUS: Pruebas en Lean de “El punto de acumulación de las convergentes es su límite”

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

Si a es un punto de acumulación de una sucesión convergente u, entonces a es el límite de u.

usando los estilos declarativo, aplicativos y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada