One_to_Many_Image_of_Set_Difference
Provedproofwikirelation-theoryset-difference
Let R ⊆ S × T be a one-to-many relation and let A and B be subsets of S. Then R[A] \ R[B] = R[A \ B]. For injective mappings, the image of a set difference equals the set difference of images.
Preamble
import Mathlib.Data.Set.Function
Formal statement
theorem One_to_Many_Image_of_Set_Difference {α β : Type _} {f : α → β} (hf : Function.Injective f) (A B : Set α) : f '' A \ f '' B = f '' (A \ B) := by sorrySource