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