Commit 2021-08-22 16:54 87f14e30

feat(topology/basic): interior of a singleton (#8784)

• add generic lemmas interior_singleton, closure_compl_singleton;
• add more lemmas and instances about ne_bot (𝓝[{x}ᶜ] x);
• rename dense_compl_singleton to dense_compl_singleton_iff_not_open, add new dense_compl_singleton that assumes [ne_bot (𝓝[{x}ᶜ] x)].