compl_compl — Mathlib

English

In any topological space, for every open set U, taking the complement twice returns U; i.e., (U^c)^c = U. Thus the complement operation on open sets is an involution.

Русский

В любом топологическом пространстве для любого открытого множества U двойной комплемент возвращает U; т.е. (U^c)^c = U. Следовательно, отображение комплемента на открытых множествах является инволюцией.

LaTeX

$$$ \\forall U \\subseteq \\alpha,\\ IsOpen(U) \\Rightarrow (U^c)^c = U $$$

Lean4

nonrec theorem compl_compl (s : Opens α) : s.compl.compl = s :=
  Opens.ext (compl_compl (s : Set α))

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