DAO: La semana en Calculemus (del 2 al 6 de mayo de 2022)

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

A continuación se muestran las soluciones.

1. Imagen de la unión

En Lean, la imagen de un conjunto s por una función f se representa por f '' s; es decir, f '' s = {y | ∃ x, x ∈ s ∧ f x = y}

Demostrar que f '' (s ∪ t) = f '' s ∪ f '' t

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

2. Teorema de Cantor

Demostrar el teorema de Cantor; es decir, que no existe ninguna aplicación suprayectiva de un conjunto en su conjunto potencia.

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