pairwise_disjoint_nhds — Mathlib

English

In a Hausdorff space, the family of neighborhoods is pairwise disjoint for distinct points.

Русский

В пространстве Хаусдорфа семейство окрестностей парно несепересекается для разных точек.

LaTeX

$$$ [T2Space X] \Rightarrow \text{Pairwise } (\operatorname{Disjoint} \text{ on } (\mathcal{N})) $$$

Lean4

theorem pairwise_disjoint_nhds [T2Space X] : Pairwise (Disjoint on (𝓝 : X → Filter X)) := fun _ _ =>
  disjoint_nhds_nhds.2

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