proposition: Lemma denseNE (T : topologicalType) (S : set T) : ~ dense S -> exists O, (exists x, open_nbhs x O) /\ (O `&` S = set0).
proof: Proof. rewrite /dense /open_nbhs. move=> /existsNP[X /not_implyP[[x Xx] /not_implyP[ Ox /forallNP A]]]. by exists X; split; [exists x | rewrite -subset0; apply/A]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed