Imagen de la intersección general

Demostrar con Lean4 que
\[ f\left[\bigcap_{i ∈ I} A_i\right] ⊆ \bigcap_{i ∈ I} f[A_i] \]

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

1. Demostración en lenguaje natural

Sea \(y\) tal que
\[ y ∈ f\left[\bigcap_{i ∈ I} Aᵢ\right] \tag{1} \]
Tenemos que demostrar que
\[ y ∈ \bigcap_{i ∈ I} f[Aᵢ] \]
Para ello, sea \(i ∈ I\), tenemos que demostrar que \(y ∈ f[Aᵢ]\).

Por (1), existe un \(x\) tal que
\begin{align}
&x ∈ \bigcap_{i ∈ I} Aᵢ \tag{2} \\
&f(x) = y \tag{3}
\end{align}
Por (2),
\[ x ∈ Aᵢ \]
y, por tanto,
\[ f(x) ∈ f[Aᵢ] \]
que, junto con (3), da que
\[ y ∈ f[Aᵢ] \]

2. Demostraciones con Lean4

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

3. Demostraciones con Isabelle/HOL

Escribe un comentario