preimage_compl_eq_image_compl — Mathlib

English

In a Boolean algebra, the preimage of a set under complement equals the image of the set under complement: compl^{-1}(s) = compl(s).

Русский

В булевой алгебре предобраз под дополнения равен образу под дополнения: compl^{-1}(s) = compl(s).

LaTeX

$$$ \\text{preimage }(\\text{compl}, s) = \\text{image }(\\text{compl}, s). $$$

Lean4

theorem preimage_compl_eq_image_compl [BooleanAlgebra α] (s : Set α) : HasCompl.compl ⁻¹' s = HasCompl.compl '' s :=
  Set.ext fun x =>
    ⟨fun h => ⟨xᶜ, h, compl_compl x⟩, fun h => Exists.elim h fun _ hy => (compl_eq_comm.mp hy.2).symm.subst hy.1⟩

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