Subset_equals_Preimage_of_Image_iff_Mapping_is_Injection
Provedcomposite-mappingsinjectionspreimages-under-mappingsproofwikisubsets
Let be a mapping. Let denote the inverse of . Then is an injection where denotes the image of under denotes the composition of and . This can be expressed in the language and notation of direct image mappings and inverse image mappings as is an injection
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Subset_equals_Preimage_of_Image_iff_Mapping_is_Injection {S T : Type _} (f : S -> T) : (forall (A : Set S), A = Set.preimage f (Set.image f A)) <-> Function.Injective f := by sorrySource