t0Space_iff_nhds_injective — Mathlib

English

A space is T0 iff the neighborhood map x ↦ 𝓝 x is injective.

Русский

Пространство является T0 тогда и только тогда, когда отображение точка → множество окрестностей инъективно.

LaTeX

$$$T0Space(X) \iff Injective(\mathcal{N}: X \to Filter X).$$$

Lean4

theorem t0Space_iff_nhds_injective (X : Type u) [TopologicalSpace X] : T0Space X ↔ Injective (𝓝 : X → Filter X) :=
  t0Space_iff_inseparable X

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