Factoring_Mapping_into_Surjection_and_Inclusion
Provedinclusion-mappingsproofwikisurjections
Every mapping f: S → T can be uniquely factored into a surjection g: S → Im(f) followed by the inclusion mapping i_T: Im(f) → T.
Preamble
import Mathlib.Data.Set.Function
Formal statement
theorem Factoring_Mapping_into_Surjection_and_Inclusion {α β : Type _} (f : α → β) : Function.Surjective (fun a => (⟨f a, Set.mem_range_self a⟩ : Set.range f)) ∧ Function.Injective (Subtype.val : Set.range f → β) := by sorrySource