theorem Metric.IsSeparated.disjoint_ball {E : Type u_1} [PseudoEMetricSpace E] {s : Set E} {ε : ENNReal} (hs : IsSeparated ε s) : s.PairwiseDisjoint fun (x : E) => EMetric.ball x (ε / 2)

theorem Metric.IsSeparated.disjoint_closedBall {E : Type u_1} [PseudoEMetricSpace E] {s : Set E} {ε : ENNReal} (hs : IsSeparated ε s) : s.PairwiseDisjoint fun (x : E) => EMetric.closedBall x (ε / 2)

@[simp]

theorem EMetric.nonempty_closedBall {E : Type u_1} [PseudoEMetricSpace E] {x : E} {r : ENNReal} : (closedBall x r).Nonempty

theorem EMetric.closedBall_add_closedBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E] (x y : E) (r s : ENNReal) : closedBall x r + closedBall y s = closedBall (x + y) (r + s)