English
If f is injective, then the image of the domain set difference equals the difference of images: f[S \ T] = f[S] \ f[T].
Русский
Если f инъективна, то образ разности равен разности образов: f[S \ T] = f[S] \ f[T].
LaTeX
$$$$ f[S \setminus T] = f[S] \setminus f[T]. $$$$
Lean4
theorem image_diff {f : α → β} (hf : Injective f) (s t : Set α) : f '' (s \ t) = f '' s \ f '' t :=
Subset.antisymm (Subset.trans (image_inter_subset _ _ _) <| inter_subset_inter_right _ <| image_compl_subset hf)
(subset_image_diff f s t)