The interior of a dense constructible set

A constructible set has nowhere dense frontier. Consequently, a dense constructible set has dense interior. This supplies the open subset of a dominant finite-presentation image used in conjunction with Chevalley's theorem.

theorem Topology.IsConstructible.isNowhereDense_frontier {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsConstructible s) : IsNowhereDense (frontier s)

The frontier of a constructible set is nowhere dense.

theorem Topology.IsConstructible.dense_interior {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsConstructible s) (hd : Dense s) : Dense (interior s)

A dense constructible set has dense interior, with no separation hypothesis.