eq_of_clusterPt_uniformity

Mathlib.Topology.UniformSpace.Separation

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

English

If ClusterPt((x,y), 𝓤α) holds, then x = y (for T0 spaces).

Русский

Если ClusterPt((x,y), 𝓤α) выполняется, то x = y (для T0 пространств).

LaTeX

$$$\text{ClusterPt}((x,y), 𝓤α) \Rightarrow x = y$$$

Lean4

theorem eq_of_clusterPt_uniformity [T0Space α] {x y : α} (h : ClusterPt (x, y) (𝓤 α)) : x = y :=
  (inseparable_iff_clusterPt_uniformity.2 h).eq

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

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

Разделы

Аффилиация

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