subset_image_diff — Mathlib

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

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