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]