mem_closedPoints_iff

Mathlib.Topology.JacobsonSpace

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

English

For any x, x belongs to closedPoints X iff {x} is closed.

Русский

Для любого x верно: x ∈ closedPoints X тогда и только тогда, когда {x} замкнуто.

LaTeX

$$$\forall x, \; x \in closedPoints X \iff IsClosed\{x\}$$$

Lean4

@[simp]
theorem mem_closedPoints_iff {x} : x ∈ closedPoints X ↔ IsClosed { x } :=
  Iff.rfl

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

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

Разделы

Аффилиация

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