Quotient_Theorem_for_Sets
Provedmapping-theoryproofwikiquotient-mappingsquotient-sets
A mapping f: S → T can be uniquely factored into a surjection, followed by a bijection, followed by an injection: f = i ∘ r ∘ q_{R_f}.
Preamble
import Mathlib.Data.Set.Function import Mathlib.Data.Setoid.Basic
Formal statement
theorem Quotient_Theorem_for_Sets {α β : Type _} (f : α → β) : (∃ (q : α → Quotient (Setoid.ker f)) (r : Quotient (Setoid.ker f) → Set.range f) (i : Set.range f → β), Function.Surjective q ∧ Function.Bijective r ∧ Function.Injective i ∧ ∀ a, i (r (q a)) = f a) := by sorrySource