f⁻¹[u ∩ v] = f⁻¹[u] ∩ f⁻¹[v]

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 con Lean4 que

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

1. Demostración en lenguaje natural

Tenemos que demostrar que, para todo \(x\),
\[ x ∈ f⁻¹[u ∩ v] ↔ x ∈ f⁻¹[u] ∩ f⁻¹[v] \]
Lo haremos mediante la siguiente cadena de equivalencias
\begin{align}
x ∈ f⁻¹[u ∩ v] &↔ f x ∈ u ∩ v \\
&↔ f x ∈ u ∧ f x ∈ v \\
&↔ x ∈ f⁻¹[u] ∧ x ∈ f⁻¹[v] \\
&↔ x ∈ f⁻¹[u] ∩ f⁻¹[v] \\
\end{align}

2. Demostraciones con Lean4

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

Escribe un comentario