Finite_Subspace_of_Dense_in_itself_Metric_Space_is_not_Open
Proveddensenessmetric-spacesproofwiki
Let M = (A, d) be a dense-in-itself metric space. Let U be a finite nonempty subset. Then U is not open.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Finite_Subspace_of_Dense_in_itself_Metric_Space_is_not_Open {X : Type _} [MetricSpace X] [Nontrivial X] {U : Set X} (hU : Set.Finite U) (hU_ne : U.Nonempty) (hdense : ∀ x : X, ¬ ∃ ε > 0, Metric.ball x ε = {x}) : ¬ IsOpen U := by sorrySource