La composición de funciones suprayectivas es suprayectiva

Demostrar con Lean4 que la composición de funciones suprayectivas es suprayectiva.

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

Demostración en lenguaje natural


Supongamos que \(f : A → B\) y \(g : B → C\) son suprayectivas. Tenemosque demostrar que
\[ (∀z ∈ C)(∃x ∈ A)[g(f(x)) = z] \]
Sea \(z ∈ C\). Por ser \(g\) suprayectiva, existe un \(y ∈ B\) tal que
\[ g(y) = z \tag{1} \]
Por ser \(f\) suprayectiva, existe un \(x ∈ A\) tal que
\[ f(x) = y \tag{2} \]
Por tanto,
\begin{align}
g(f(x)) &= g(y) &&\text{[por (2)]} \\
&= z &&\text{[por (1)]}
\end{align}

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

Escribe un comentario