image_diff — Mathlib

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)

Похожие утверждения