toClopens — Mathlib

English

Reinterpret a compact-open as a clopen in T2 spaces.

Русский

Преобразование компакт-открытого множества в открытое и закрытое (clopen) в пространстве T2.

LaTeX

$$$\mathrm{toClopens}(s) = \langle s, s\text{ isCompact}.isClosed, s\text{ isOpen} \rangle$$$

Lean4

/-- Reinterpret a compact open as a clopen. -/
@[simps]
def toClopens [T2Space α] (s : CompactOpens α) : Clopens α :=
  ⟨s, s.isCompact.isClosed, s.isOpen⟩

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