Theorems · Theorem · general topology

IsOpen.dense

∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [PreirreducibleSpace X], IsOpen s → s.Nonempty → Dense s

In a (pre)irreducible space, a nonempty open set is dense.

Defined in

Mathlib.Topology.Irreducible

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreirreducibleSpace