Bijection_iff_Left_and_Right_Inverse
Provedbijectionsinverse-mappingsproofwiki
Let f: S → T be a mapping. f is a bijection if and only if there exist g₁, g₂: T → S such that g₁ ∘ f = I_S and f ∘ g₂ = I_T.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Bijection_iff_Left_and_Right_Inverse {α β : Type _} (f : α → β) : Function.Bijective f ↔ (∃ g₁ : β → α, g₁ ∘ f = id) ∧ (∃ g₂ : β → α, f ∘ g₂ = id) := by sorrySource