compl_image — Mathlib

English

The image of the complement map equals the preimage under the complement map: image (compl) = preimage (compl).

Русский

Образ комплемента как отображения равен предобразу комплемента: image(compl) = preimage(compl).

LaTeX

$$$\\operatorname{image}(\\mathrm{compl}) = \\operatorname{preimage}(\\mathrm{compl})$$$

Lean4

theorem compl_image : image (compl : Set α → Set α) = preimage compl :=
  image_eq_preimage_of_inverse compl_compl compl_compl

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