ForMatUS: Pruebas en Lean de “Hay infinitos términos arbitrariamente próximos a los puntos de acumulación”

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

Si a es un punto de acumulación de la sucesión u, entonces

∀ ε > 0, ∀ N, ∃ n ≥ N, |u n – a| ≤ ε

usando los estilos declarativo, aplicativo y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada