ForMatUS: Pruebas en Lean de la intersección sobre unión general: C ∩ (⋃i, A i) = (⋃ i, C ∩ A i)

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de la propiedad

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

ForMatUS: Pruebas en Lean de la distributiva de la intersección general sobre la intersección

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 4 pruebas en Lean de la propiedad distributiva de la intersección general sobre la intersección :

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

ForMatUS: Pertenencia a uniones e intersecciones de familias en Lean

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de la caracterización de la pertenencia a uniones o intersecciones de familias de conjuntos.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

ForMatUS: Unión e intersección de familias de conjuntos en Lean

He añadido a la lista Lógica con Lean el vídeo en el que se comentan cómo definir en Lean la unión e intersección de familias de conjuntos y caracterizar la relación de pertenencia.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

ForMatUS: Pruebas en Lean de (A ∩ Bᶜ) ∪ B = A ∪ B

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 4 pruebas en Lean de la propiedad

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada