En el vídeo se prueba en Lean las siguientes propiedades de los números reales:
- Si 0 ≤ a, entonces b ≤ a + b.
- Si 0 ≤ b, entonces a ≤ a + b.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
En el vídeo se presentan 12 demostraciones en Lean de la siguiente propiedad:
Sean a, b y c números reales. Si a ≤ b, entonces a + c ≤ b + c.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
En el vídeo se presentan 11 demostraciones en Lean de la siguiente propiedad:
Sean a, b y c números reales. Si a ≤ b, entonces c + a ≤ c + b.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
En el vídeo se comentan distintas demostraciones sobre la eliminación de la disyunción en Lean: con tácticas, con término de prueba y automáticas.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
En el vídeo se comentan distintas demostraciones sobre la introducción de la conjunción en Lean: con tácticas, con términos de prueba, estructuradas y automática.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo