instHasCompl — Mathlib

English

For every clopen subset s of α, its complement sᶜ is also clopen; i.e., Clopens(α) is closed under complement.

Русский

Для любого клопного множества s в α его дополнение sᶜ также является клопным; то есть множество клопных множеств замкнуто относительно дополнения.

LaTeX

$$$\forall s \in \mathrm{Clopens}(\alpha):\ s^{c} \in \mathrm{Clopens}(\alpha).$$$

Lean4

instance : HasCompl (Clopens α) :=
  ⟨fun s => ⟨sᶜ, s.isClopen.compl⟩⟩

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