mathlib3

e00afed4 - feat(topology/metric_space): turn `nonempty_ball` into an `iff` (#8747)

feat(topology/metric_space): turn `nonempty_ball` into an `iff` (#8747) * add `set.univ_pi_empty`; * turn `metric.nonempty_ball` into an `iff`, mark it with `@[simp]`; add `metric.ball_eq_empty` * do the same thing to `closed_ball`s; * add primed versions of `metric.ball_pi` and `metric.closed_ball_pi`.