Commit 2021-12-28 13:53 d053d57a
View on Github →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
.