En el vídeo se comentan 6 demostraciones en Lean de la siguiente propiedad:
Sean a, b y c números reales. Si 0 ≤ c y a ≤ b, entonces ac ≤ bc.
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 pruebas en Lean de la siguiente propiedad:
Sean a, b, c y d números reales. Si a ≤ b y c ≤ d, entonces a + c ≤ b + d.
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 pruebas en Lean de la siguiente propiedad:
Sean a y b números reales. Si 0 ≤ a y 0 ≤ b, entonces 0 ≤ 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 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