Left_Inverse_Mapping_is_Surjection
Provedleft-inverse-mappingsproofwikisurjections
Let f: S → T be an injection. Let g: T → S be a left inverse of f. Then g is a surjection.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Left_Inverse_Mapping_is_Surjection {α β : Type _} {f : α → β} {g : β → α} (hf : Function.Injective f) (hgf : g ∘ f = id) : Function.Surjective g := by sorrySource