Imagen inversa de la intersección general

Demostrar con Lean4 que
\[ f⁻¹\left[\bigcap_{i \in I} B_i\right] = \bigcap_{i \in I} f⁻¹[B_i] \]

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

1. Demostración en lenguaje natural

Se demuestra mediante la siguiente cadena de equivalencias
\begin{align}
x ∈ f⁻¹\left[\bigcap_{i \in I} B_i\right]
&↔ f(x) ∈ \bigcap_{i \in I} B_i \\
&↔ (∀ i) f(x) ∈ B_i \\
&↔ (∀ i) x ∈ f⁻¹[B_i] \\
&↔ x ∈ \bigcap_{i \in I} f⁻¹[B_i]
\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