Imagen inversa de la intersección

En Lean, la imagen inversa de un conjunto s (de elementos de tipo por la función f (de tipo α → β) es el conjunto f ⁻¹' s de elementos x (de tipo α) tales que f x ∈ s.

Demostrar que f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v

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