compl_compl — Mathlib

English

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

Русский

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

LaTeX

$$$ \\forall F \\subseteq \\alpha,\\ IsClosed(F) \\Rightarrow (F^c)^c = F $$$

Lean4

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

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