∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal),
  Metric.closedEBall x r ×ˢ Metric.closedEBall y r = Metric.closedEBall (x, y) r