feat(topology/basic): Lim_spec etc. cleanup (#4545)
Fixes #4543
See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/More.20point.20set.20topology.20questions/near/212757136)
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
