inseparable_iff_eq

Mathlib.Topology.Separation.Basic

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

English

In a T0 space, two points are inseparable if and only if they are equal.

Русский

В T0-пространстве две точки неразделимы тогда и только тогда, когда они равны.

LaTeX

$$$Inseparable(x,y) \iff x=y$ [T0Space X].$$

Lean4

theorem inseparable_iff_eq [T0Space X] {x y : X} : Inseparable x y ↔ x = y :=
  nhds_injective.eq_iff

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

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

Разделы

Аффилиация

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