Mapping_is_Injection_if_its_Direct_Image_Mapping_is_Injection
Proveddirect-image-mappingsinjectionsproofwiki
Let f: S → T be a mapping. If the direct image mapping of f is an injection, then f is also an injection.
Preamble
import Mathlib.Data.Set.Function
Formal statement
theorem Mapping_is_Injection_if_its_Direct_Image_Mapping_is_Injection {α : Type _} {β : Type _} {f : α → β} (hf : Function.Injective (Set.image f)) : Function.Injective f := by sorrySource