t2Space_iff_nhds — Mathlib

English

For a Hausdorff space, a set of points is pairwise disjoint with respect to nhds.

Русский

Для пространства Хаусдорфа множество точек попарно нес пересекается по окрестностям.

LaTeX

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

Lean4

theorem t2Space_iff_nhds : T2Space X ↔ Pairwise fun x y : X => ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V := by
  simp only [t2Space_iff_disjoint_nhds, Filter.disjoint_iff, Pairwise]

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