image_compl_subset — Mathlib

English

If f is injective, then the image of the complement of S is contained in the complement of the image of S: f[S^c] ⊆ (f[S])^c.

Русский

Если f инъективна, то образ дополнения S содержится в дополнении образа S: f[S^c] ⊆ (f[S])^c.

LaTeX

$$$$ f[S^{c}] \subseteq (f[S])^{c}. $$$$

Lean4

theorem image_compl_subset {f : α → β} {s : Set α} (H : Injective f) : f '' sᶜ ⊆ (f '' s)ᶜ :=
  Disjoint.subset_compl_left <| by simp [disjoint_iff_inf_le, ← image_inter H]

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