Quotient_Theorem_for_Surjections
Provedproofwikiquotient-mappingsquotient-setssurjections
Let f: S → T be a surjection. Then there is one and only one bijection r: S/R_f → T such that r ∘ q_{R_f} = f.
Preamble
import Mathlib.Logic.Function.Basic import Mathlib.Data.Setoid.Basic
Formal statement
theorem Quotient_Theorem_for_Surjections {α β : Type _} {f : α → β} (hf : Function.Surjective f) : Function.Bijective (Quotient.lift f (fun a b h => h) : Quotient (Setoid.ker f) → β) := by sorrySource