toCloseds — Mathlib

English

A nonempty compact can be viewed as a closed set in a Hausdorff space: toCloseds(s) = ⟨s, s.isCompact.isClosed⟩.

Русский

Непустый компакт можно рассматривать как замкнутое множество в Хаусдорфовом пространстве: toCloseds(s) = ⟨s, s.isCompact.isClosed⟩.

LaTeX

$$$[T2Space \\alpha] (s : \\mathrm{NonemptyCompacts}(\\alpha)) \\Rightarrow \\text{toCloseds }(s) = \\langle s, s.isCompact.isClosed \\rangle$$$

Lean4

/-- Reinterpret a nonempty compact as a closed set. -/
def toCloseds [T2Space α] (s : NonemptyCompacts α) : Closeds α :=
  ⟨s, s.isCompact.isClosed⟩

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