mathlib3

dcf22508 - Split `infinite_of_mem_nhds` to extract a useful lemma (#17971)

Split `infinite_of_mem_nhds` to extract a useful lemma (#17971) Nothing new mathematically since the new lemma is just the contraposition of `infinite_of_mem_nhds`, but the proof of the latter actually goes through a proof of the former so it makes more sense to reorganize things like that. Requested by @xroblot on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/is_open.20.7Ba.7D.20from.20finite.20balls)