t2_separation_nhds — Mathlib

English

In a Hausdorff space, for distinct points, there exist disjoint neighborhoods with the points in them.

Русский

В пространстве Хаусдорфа для различных точек существуют непересекающиеся окрестности вокруг них.

LaTeX

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

Lean4

theorem t2_separation_nhds [T2Space X] {x y : X} (h : x ≠ y) : ∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ Disjoint u v :=
  let ⟨u, v, open_u, open_v, x_in, y_in, huv⟩ := t2_separation h
  ⟨u, v, open_u.mem_nhds x_in, open_v.mem_nhds y_in, huv⟩

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