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