singleton — Mathlib

English

The closed-set corresponding to a singleton is exactly the singleton set {x}, which is closed.

Русский

Замкнутое множество, соответствующее одиночному элементу, равно множеству {x} и является замкнутым.

LaTeX

$$$\text{singleton}(x) = \langle \{x\}, \text{isClosed}(\{x\})\rangle.$$$

Lean4

/-- The term of `TopologicalSpace.Closeds α` corresponding to a singleton. -/
@[simps]
def singleton [T1Space α] (x : α) : Closeds α :=
  ⟨{ x }, isClosed_singleton⟩

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