t1Space — Mathlib

English

For distinct points x ≠ y in a Hausdorff space, there exist neighborhoods u of x and v of y that are disjoint.

Русский

Для разных точек x ≠ y в пространстве Хаусдорфа существуют окрестности u вокруг x и v вокруг y, которые не пересекаются.

LaTeX

$$$ [T2Space X] \forall x \neq y, \exists u,v, u\in \mathcal{N}(x) \land v\in \mathcal{N}(y) \land Disjoint(u,v) $$$

Lean4

instance (priority := 100) t1Space [T2Space X] : T1Space X :=
  t1Space_iff_disjoint_pure_nhds.mpr fun _ _ hne =>
    (disjoint_nhds_nhds.2 hne).mono_left <|
      pure_le_nhds
        _
          -- see Note [lower instance priority]

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