DAO: La semana en Calculemus (del 18 al 23 de abril)

Esta semana he publicado en Calculemus las soluciones de los siguientes problemas:

A continuación se muestran las soluciones.

1. Propiedad de monotonía de la intersección

Demostrar que la intersección es monótona por la izquierda; es decir, si s ⊆ t, entonces s ∩ u ⊆ t ∩ u.

Para ello, completar la siguiente teoría de Lean:

Soluciones con Lean

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

La construcción de las demostraciones se muestra en el siguiente vídeo

Soluciones con Isabelle/HOL

2. Propiedad distributiva de la intersección sobre la unión

Demostrar que s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u).

Para ello, completar la siguiente teoría de Lean:

Soluciones con Lean

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

La construcción de las demostraciones se muestra en el siguiente vídeo

Soluciones con Isabelle/HOL

3. Diferencia de diferencia de conjuntos

Demostrar que (s \ t) \ u ⊆ s \ (t ∪ u)

Para ello, completar la siguiente teoría de Lean:

Soluciones con Lean

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

La construcción de las demostraciones se muestra en el siguiente vídeo

Soluciones con Isabelle/HOL