image_compl_eq — Mathlib

English

If f is bijective, then the image of the complement of S equals 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}] = (f[S])^{c}. $$$$

Lean4

theorem image_compl_eq {f : α → β} {s : Set α} (H : Bijective f) : f '' sᶜ = (f '' s)ᶜ :=
  Subset.antisymm (image_compl_subset H.1) (subset_image_compl H.2)

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