Equivalence_of_Definitions_of_Closure_of_Topological_Subspace

Proved

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

proofwikiset-closures

Let $T = \struct {S, \tau}$ be a topological space. Let $H \subseteq S$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Equivalence_of_Definitions_of_Closure_of_Topological_Subspace {α : Type _} [TopologicalSpace α] (s : Set α) : closure s = ⋂₀ {t | IsClosed t ∧ s ⊆ t} := by sorry

Source

https://proofwiki.org/wiki/Equivalence_of_Definitions_of_Closure_of_Topological_Subspace

View graph