Finite_Subset_of_Metric_Space_has_no_Limit_Points
Provedmetric-spacesproofwiki
Let M = (A, d) be a metric space. Let X be a finite subset of A. Then X has no limit points.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Finite_Subset_of_Metric_Space_has_no_Limit_Points {X : Type _} [MetricSpace X] {S : Set X} (hS : Set.Finite S) (x : X) (hx : x ∈ closure S) (hx2 : x ∉ S) : False := by sorrySource