Surjection_if_Composite_is_Surjection
Provedcomposite-mappingsproofwikisurjections
Let f: S₁ → S₂ and g: S₂ → S₃ be mappings such that g ∘ f is a surjection. Then g is a surjection.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Surjection_if_Composite_is_Surjection {α β γ : Type _} {f : α → β} {g : β → γ} (h : Function.Surjective (g ∘ f)) : Function.Surjective g := by sorrySource