Point_in_Finite_Hausdorff_Space_is_Isolated
Provedhausdorff-spacesisolated-pointsproofwiki
Let T = (S, tau) be a Hausdorff space. Let X be a finite subset of S. Let x be in X. Then x is an isolated point of X.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Point_in_Finite_Hausdorff_Space_is_Isolated {X : Type _} [TopologicalSpace X] [T2Space X] {S : Set X} (hS : Set.Finite S) (x : X) (hx : x ∈ S) : ∃ U ∈ nhds x, U ∩ S = {x} := by sorrySource