Theorems · Theorem · general topology

dense_compl_singleton_iff_not_open

∀ {X : Type u} [inst : TopologicalSpace X] {x : X}, Dense {x}ᶜ ↔ ¬IsOpen {x}

Complement to a singleton is dense if and only if the singleton is not an open set.

Defined in

Mathlib.Topology.Closure

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace