Right_Inverse_Mapping_is_Injection
Provedinjectionsproofwikiright-inverse-mappings
Let f: S → T be a mapping. Let g: T → S be a right inverse of f. Then g is an injection.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Right_Inverse_Mapping_is_Injection {α β : Type _} {f : α → β} {g : β → α} (hfg : f ∘ g = id) : Function.Injective g := by sorrySource