mathlib

35f1f637 - doc(topology/basic): docstrings for nhds and a few related lemmas (#3548)

doc(topology/basic): docstrings for nhds and a few related lemmas (#3548) `nhds` was the only `def` in the file which didn't have an explanation, so I documented it. I also went ahead and documented a few related lemmas which I felt were worth calling out. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>