closedPoints

Mathlib.Topology.JacobsonSpace

URI: https://scilib.ai/kg/mathlib#closedPoints

English

The closed points are those x ∈ X for which the singleton {x} is closed.

Русский

Замкнутые точки — это такие x ∈ X, что множество {x} замкнуто.

LaTeX

$$$\text{def closedPoints}(X) := \{x \in X : IsClosed\{x\}\}$$$

Lean4

/-- The set of closed points. -/
def closedPoints : Set X :=
  setOf (IsClosed {·})

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru