ForMatUS: Conectivas y desigualdades en Lean

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo Conectivas y desigualdades en Lean en el se comentan las demostraciones en Lean de algunas de las propiedades de las desigualdades de los números reales estudiadas en vídeos anteriores, pero formuladas con conectivas. Concretamente, se demuestran las 5 propiedades siguientes:

Sean a, b y c números reales.

  1. 0 ≤ a → b ≤ a + b
  2. 0 ≤ b → a ≤ a + b
  3. (0 ≤ a ∧ 0 ≤ b) → 0 ≤ a + b
  4. 0 ≤ a → (0 ≤ b → 0 ≤ a + b)
  5. Si (0 ≤ a ∧ 0 ≤ b) → 0 ≤ a + b, entonces 0 ≤ a → (0 ≤ b → 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