nhds_injective

Mathlib.Topology.Separation.Basic

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

English

If X is T0, then the neighborhood map 𝓝 is injective.

Русский

Если X является T0, то отображение окрестностей 𝓝 инъективно.

LaTeX

$$[T0Space X] ⇒ Injective(𝓝: X → Filter X).$$

Lean4

theorem nhds_injective [T0Space X] : Injective (𝓝 : X → Filter X) :=
  (t0Space_iff_nhds_injective X).1 ‹_›

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

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

Разделы

Аффилиация

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