t2Space_iff_disjoint_nhds — Mathlib

English

Hausdorff property is equivalent to disjoint neighborhoods of distinct points.

Русский

Свойство Хаусдорфа эквивалентно тому, что для различных точек их окрестности парно не пересекаются.

LaTeX

$$$ [\text{T2Space}(X)] \iff \operatorname{Pairwise}(\lambda x\,y. Disjoint(\mathcal{N}(x), \mathcal{N}(y))) $$$

Lean4

theorem t2Space_iff_disjoint_nhds : T2Space X ↔ Pairwise fun x y : X => Disjoint (𝓝 x) (𝓝 y) :=
  by
  refine (t2Space_iff X).trans (forall₃_congr fun x y _ => ?_)
  simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens y), ← exists_and_left, and_assoc, and_comm,
    and_left_comm]

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