ForMatUS: Pruebas en Lean de P → Q, P → ¬Q ⊢ ¬P

He añadido a la lista Lógica con Lean el vídeo Pruebas en Lean de P → Q, P → ¬Q ⊢ ¬P en el que se comentan 11 pruebas en Lean de la siguiente propiedad

P → Q, P → ¬Q ⊢ ¬P

usando las reglas del condicional y de la negación.

Los enlaces correspondientes son:

• a la sesión en Lean Web,
• al código,
• al libro “Lógica con Lean” y
• al repositorio en GitHub “Lógica con Lean”.

A continuación, se muestra el vídeo