English
In a locally compact Hausdorff space, for distinct points x ≠ y, there exist disjoint neighborhoods which are compact around each point.
Русский
В локально компактном хаусдорфовом пространстве для различных x ≠ y существуют непересекающиеся компактные окрестности вокруг каждой точки.
LaTeX
$$$ [\text{LocallyCompactSpace}(X)] [T2Space X] \forall x \neq y, \exists u,v\ (u \in 𝓝 x) (v \in 𝓝 y) (IsCompact u) (IsCompact v) (Disjoint u v) $$$
Lean4
theorem t2_separation_compact_nhds [LocallyCompactSpace X] [T2Space X] {x y : X} (h : x ≠ y) :
∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v := by
simpa only [exists_prop, ← exists_and_left, and_comm, and_assoc, and_left_comm] using
((compact_basis_nhds x).disjoint_iff (compact_basis_nhds y)).1 (disjoint_nhds_nhds.2 h)
