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

Soluciones con Isabelle/HOL

Escribe un comentario