Open_Set_Less_One_Point_is_Open
Provedmetric-spacesopen-setsproofwiki
Let M = (A, d) be a metric space. Let U be an open set of M and a be in U. Then U \ {a} is open in M.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Open_Set_Less_One_Point_is_Open {X : Type _} [MetricSpace X] {U : Set X} (hU : IsOpen U) (a : X) : IsOpen (U \ {a}) := by sorrySource