compl_compl_image — Mathlib

English

For a Boolean algebra α, the double complement image returns the original set: compl''(compl'' s) = s.

Русский

Для булевой алгебры α двойной образ дополнения возвращает исходное множество: compl''(compl'' s) = s.

LaTeX

$$$ \\operatorname{compl}''(\\operatorname{compl}'' s) = s. $$$

Lean4

theorem compl_compl_image [BooleanAlgebra α] (s : Set α) : HasCompl.compl '' (HasCompl.compl '' s) = s := by
  rw [← image_comp, compl_comp_compl, image_id]

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