subset_image_compl — Mathlib

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]

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