source
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)
source
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)
source
@[simp]
theorem EMetric.nonempty_closedBall {E : Type u_1} [PseudoEMetricSpace E] {x : E} {r : ENNReal} :
(closedBall x r).Nonempty
source
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)