of_singleton_finset — Mathlib

English

A singleton set is SeparatedNhds from any finite set not containing its element in a Hausdorff space.

Русский

Одиночное множество отделимо от любого конечного множества, не содержащего его элемента, в Хаусдорфовом пространстве.

LaTeX

$$$[T2Space X] \\; x\\in X, s\\in Finset X, x\\notin s\\Rightarrow SeparatedNhds ({x}:Set X) s.$$$

Lean4

theorem of_singleton_finset [T2Space X] {x : X} {s : Finset X} (h : x ∉ s) : SeparatedNhds ({ x } : Set X) s :=
  mod_cast .of_finset_finset { x } s (Finset.disjoint_singleton_left.mpr h)

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