Pruebas en Lean de “Un número es par si, y sólo si, lo es su cuadrado”

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

Un número es par si, y sólo si, lo es su cuadrado-

usando los estilos declarativo, aplicativo y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

Pruebas en Lean de “La relación menor es irreflexiva en los reales”

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

La relación menor es irreflexiva en los reales

usando los estilos declarativo, funcional, aplicativo y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

Pruebas en Lean de “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”

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

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.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

Pruebas en Lean de “Toda sucesión convergente es una sucesión de Cauchy”

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

Toda sucesión convergente es una sucesión de Cauchy

usando los estilos aplicativo y declarativo.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

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