lean_workbook_plus_8633
ProvedProve that the closure of a set E in a metric space X, denoted by , is closed. Use the definition that the closure of E is the union of E and the set of all limit points of E.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8633 {X : Type*} [MetricSpace X] (E : Set X) : IsClosed (closure E) := by sorrySource