s ⊆ f⁻¹[f[s]​]

Demostrar que si \(s\) es un subconjunto del dominio de la función \(f\), entonces \(s\) está contenido en la imagen inversa de la imagen de \(s\) por \(f\); es decir,
\[ s ⊆ f⁻¹[f[s]] \]

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

1. Demostración en lenguaje natural

Se demuestra mediante la siguiente cadena de implicaciones
\begin{align}
x ∈ s &⟹ f(x) ∈ f[s] \\
&⟹ x ∈ f⁻¹[f[s]]
\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