Closure_of_Topological_Closure_equals_Closure

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

proofwikiset-closures

Let $T$ be a topological space. Let $H \subseteq T$ . Then $\left({H^-}\right)^- = H^-$ where $H^-$ denotes the closure of $H$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Closure_of_Topological_Closure_equals_Closure {α : Type _} [TopologicalSpace α] (s : Set α) : closure (closure s) = closure s := by sorry

Source