Commit 2022-01-17 07:55 83eff323

feat(topology/metric_space): more lemmas about disjoint balls (#11506)

• drop unused lemmas metric.ball_disjoint and metric.ball_disjoint_same; the former was a duplicate of metric.ball_disjoint_ball;
• add metric.closed_ball_disjoint_ball, metric.closed_ball_disjoint_closed_ball.