Commit 2021-12-28 13:53 d053d57a

feat(topology): missing lemmas for Kyle (#11076) Discussion on Zulip revealed gaps in library. This PR fills those gaps and related ones discovered on the way. It will simplify #11072. Note that it unprotects topological_space.nhds_adjoint and puts it into the root namespace. I guess this was protected because it was seen only as a technical tools to prove properties of nhds.