Injection_iff_Left_Inverse
Provedinjectionsleft-inverse-mappingsproofwiki
A mapping f: S → T, S ≠ ∅ is an injection if and only if there exists g: T → S such that g ∘ f = I_S, i.e. f has a left inverse.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Injection_iff_Left_Inverse {α β : Type _} [Nonempty α] (f : α → β) : Function.Injective f ↔ ∃ g : β → α, g ∘ f = id := by sorrySource