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

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

The closed balls of radius ε / 2 around the points of an ε-separated set are pairwise disjoint.

@[simp]

theorem Metric.nonempty_closedEBall {E : Type u_1} [PseudoEMetricSpace E] {x : E} {r : ENNReal} : (closedEBall x r).Nonempty

theorem closedEBall_add_closedEBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E] (x y : E) (r s : ENNReal) : Metric.closedEBall x r + Metric.closedEBall y s = Metric.closedEBall (x + y) (r + s)