Saltar al Contenido

Vestigium

Cuaderno de Investigación en Lógica Computacional

Facebook Twitter Instagram
Vestigium
Cuaderno de Investigación en Lógica Computacional

Autor: José A. Alonso

ForMatUS: La suma de no negativos es expansiva (en Lean)

PorJosé A. Alonso 21 agosto 202029 agosto 2020

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

ForMatUS: Monotonía de la suma por la derecha en Lean

PorJosé A. Alonso 21 agosto 202029 agosto 2020

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

ForMatUS: Monotonía de la suma por la izquierda en Lean

PorJosé A. Alonso 20 agosto 202029 agosto 2020

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

ForMatUS: Eliminación de la disyunción en Lean

PorJosé A. Alonso 19 agosto 202029 agosto 2020

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

ForMatUS: Introducción de la conjunción en Lean

PorJosé A. Alonso 19 agosto 202029 agosto 2020

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

Navegación de Página

Previous PagePrevio 1 … 52 53 54 55 56 … 411 Next PageSiguiente
junio 2025
L M X J V S D
 1
2345678
9101112131415
16171819202122
23242526272829
30  
« May    
  • La semana en Calculemus (25 de mayo de 2024)25 mayo 2024
  • La semana en Calculemus (18 de mayo de 2024)18 mayo 2024
  • La semana en Calculemus (11 de mayo de 2024)11 mayo 2024
  • La semana en Calculemus (4 de mayo de 2024)4 mayo 2024
  • Resumen de lecturas compartidas durante abril de 20244 mayo 2024
  • El mes de abril en Exercitium (Ejercicios con Haskell y Python)3 mayo 2024
  • La semana en Calculemus (27 de abril de 2024)27 abril 2024
  • La semana en Calculemus (21 de abril de 2024)21 abril 2024
  • El mes de marzo en Exercitium (Ejercicios con Haskell y Python)2 abril 2024
  • La semana en Calculemus (16 de marzo de 2024)16 marzo 2024
  • La semana en Calculemus (9 de marzo de 2024)9 marzo 2024
  • La semana en Calculemus (2 de marzo de 2024)2 marzo 2024
  • La semana en Calculemus (24 de febrero de 2024)24 febrero 2024
  • La semana en Calculemus (3 de febrero de 2024)3 febrero 2024
  • La semana en Calculemus (27 de enero de 2024)27 enero 2024
  • La semana en Calculemus (20 de enero de 2024)20 enero 2024
  • La semana en Calculemus (13 de enero de 2024)13 enero 2024
  • La semana en Calculemus (6 de enero de 2024)6 enero 2024
  • La semana en Calculemus (30 de diciembre de 2023)30 diciembre 2023
  • La semana en Calculemus (10 de diciembre de 2023)10 diciembre 2023

Correo electrónico

Introduce tu correo electrónico para suscribirte a este blog y recibir notificaciones de nuevas entradas.

RSS feed

© 2010-2025 Vestigium

Scroll to top
Búsqueda