pairwiseDisjoint_nhds — Mathlib

English

In a Hausdorff space, a set of points can be assigned neighborhood separations pairwise.

Русский

В пространстве Хаусдорфа множество точек можно снабдить попарно разделяющими окрестностями.

LaTeX

$$$ \forall s\subseteq X, [T2Space X] \Rightarrow s.PairwiseDisjoint (\mathcal{N}) $$$

Lean4

protected theorem pairwiseDisjoint_nhds [T2Space X] (s : Set X) : s.PairwiseDisjoint 𝓝 :=
  pairwise_disjoint_nhds.set_pairwise s

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