Surjection_iff_Right_Inverse
Provedproofwikiright-inverse-mappingssurjections
A mapping f: S → T, S ≠ ∅ is a surjection if and only if there exists g: T → S such that f ∘ g = I_T, i.e. f has a right inverse.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Surjection_iff_Right_Inverse {α β : Type _} [Nonempty α] (f : α → β) : Function.Surjective f ↔ ∃ g : β → α, f ∘ g = id := by sorrySource