not_isOpen_singleton

Mathlib.Topology.ClusterPt

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

English

A non-isolated point x cannot have {x} open.

Русский

Неизолированная точка x не может иметь открытым множество {x}.

LaTeX

$$$\neg IsOpen\{x\}$$$

Lean4

theorem not_isOpen_singleton (x : X) [NeBot (𝓝[≠] x)] : ¬IsOpen ({ x } : Set X) :=
  dense_compl_singleton_iff_not_open.1 (dense_compl_singleton x)

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

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

Разделы

Аффилиация

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