Region_Less_One_Point_is_Region
Disprovedmetric-spacesproofwikitopology
Let M be a dense-in-itself metric space. Let R be a region (connected open set). Let x be in R. Then R \ {x} is also a region.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Region_Less_One_Point_is_Region {X : Type _} [MetricSpace X] {R : Set X} (hR_open : IsOpen R) (hR_conn : IsConnected R) (x : X) (hx : x ∈ R) (hdense : ∀ y : X, ¬ ∃ ε > 0, Metric.ball y ε = {y}) : IsConnected (R \ {x}) := by sorrySource