Topological_Closure_is_Closed

Proved

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

closed-setsproofwikiset-closures

Let $T$ be a topological space. Let $H \subseteq T$ . Then the closure $\map \cl H$ of $H$ is closed in $T$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source