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⟩