mathlib3

72e151d8 - feat(topology/uniform_space): is_closed_of_spread_out (#7538)

feat(topology/uniform_space): is_closed_of_spread_out (#7538) See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/integers.20are.20closed.20in.20reals)