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]