Nowhere_Dense_iff_Complement_of_Closure_is_Everywhere_Dense

Proved

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

densenessproofwikiset-closures

Let $T = \struct {S, \tau}$ be a topological space. Let $H \subseteq S$ . Then $H$ is nowhere dense in $T$ $S \setminus H^-$ is everywhere dense in $T$ , where $H^-$ denotes the closure of $H$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Nowhere_Dense_iff_Complement_of_Closure_is_Everywhere_Dense {α : Type _} [TopologicalSpace α] (s : Set α) : interior (closure s) = ∅ ↔ Dense (closure s)ᶜ := by sorry

Source

https://proofwiki.org/wiki/Nowhere_Dense_iff_Complement_of_Closure_is_Everywhere_Dense

View graph