eq_of_nhds_neBot

Mathlib.Topology.Separation.Hausdorff

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

English

In a Hausdorff space, the neighborhoods of distinct points are pairwise disjoint.

Русский

В пространстве Хаусдорфа окрестности различных точек парно расходятся.

LaTeX

$$$ [T2Space X] :\ Pairwise (Disjoint on (\mathcal{N})) $$$

Lean4

theorem eq_of_nhds_neBot [T2Space X] {x y : X} (h : NeBot (𝓝 x ⊓ 𝓝 y)) : x = y :=
  t2_iff_nhds.mp ‹_› h

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

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

Разделы

Аффилиация

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