instHasCompl — Mathlib

English

There is a complementation operation on CompactOpens α, sending a compact-open set to its complement which is again compact-open.

Русский

Существование операции дополнения на CompactOpens α; комплемент компактно-открытого множества снова компактно-открыт.

LaTeX

$$HasCompl(CompactOpens(α))$$

Lean4

instance instHasCompl : HasCompl (CompactOpens α) where
  compl s := ⟨⟨sᶜ, s.isOpen.isClosed_compl.isCompact⟩, s.isCompact.isClosed.isOpen_compl⟩

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