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:
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := by sorry |
Read More «La composición de funciones suprayectivas es suprayectiva»