t2_separation — Mathlib

English

In a Hausdorff space, every finite subset can be separated by open neighborhoods.

Русский

В пространстве Хаусдорфа каждая конечная подмножество может быть разделено открытыми окрестностями.

LaTeX

$$$ [T2Space X] \Rightarrow \forall s \text{ finite}, \exists U: X \to \mathcal{P}(X), (\forall x, x \in U(x) \land IsOpen(U(x))) \land s.PairwiseDisjoint U $$$

Lean4

/-- Points of a finite set can be separated by open sets from each other. -/
theorem t2_separation [T2Space X] {s : Set X} (hs : s.Finite) :
    ∃ U : X → Set X, (∀ x, x ∈ U x ∧ IsOpen (U x)) ∧ s.PairwiseDisjoint U :=
  s.pairwiseDisjoint_nhds.exists_mem_filter_basis hs nhds_basis_opens

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