Composite_of_Surjections_is_Surjection
Provedcomposite-mappingsproofwikisurjections
A composite of surjections is a surjection. That is, if g and f are surjections, then so is f ∘ g.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Composite_of_Surjections_is_Surjection {α β γ : Type _} {f : β → γ} {g : α → β} (hf : Function.Surjective f) (hg : Function.Surjective g) : Function.Surjective (f ∘ g) := by sorrySource