English
If f is injective, then the image of the set difference equals the set difference of the 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 subset_image_diff (f : α → β) (s t : Set α) : f '' s \ f '' t ⊆ f '' (s \ t) :=
by
rw [diff_subset_iff, ← image_union, union_diff_self]
exact image_mono subset_union_right