Restriction_of_Mapping_to_Image_is_Surjection
Provedproofwikirestrictionssurjections
Let f: S → T be a mapping. Let g: S → Im(f) be the restriction of f to S × Im(f). Then g is a surjection.
Preamble
import Mathlib.Data.Set.Function
Formal statement
theorem Restriction_of_Mapping_to_Image_is_Surjection {α β : Type _} (f : α → β) : Function.Surjective (fun a => (⟨f a, Set.mem_range_self a⟩ : Set.range f)) := by sorrySource