mathlib

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

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`.