Point_in_Finite_Metric_Space_is_Isolated
Provedfinite-metric-spacesisolated-pointsproofwiki
Let M = (A, d) be a metric space. Let X be a finite subset of A, and 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_Metric_Space_is_Isolated {X : Type _} [MetricSpace X] {S : Set X} (hS : Set.Finite S) (x : X) (hx : x ∈ S) : ∃ ε > 0, ∀ y ∈ S, y ≠ x → dist x y ≥ ε := by sorrySource