Commit 2021-08-21 19:52 e00afed4

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_balls;
• add primed versions of metric.ball_pi and metric.closed_ball_pi.