English
If f is surjective, then the complement of the image of S is contained in the image of the complement: (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 subset_image_compl {f : α → β} {s : Set α} (H : Surjective f) : (f '' s)ᶜ ⊆ f '' sᶜ :=
compl_subset_iff_union.2 <| by
rw [← image_union]
simp [image_univ_of_surjective H]