feat(topology/metric_space/{basic,emetric_space}): product of balls o…

…f the same size (#5846)

src/topology/metric_space/basic.lean

@@ -1059,6 +1059,14 @@ instance prod.metric_space_max [metric_space β] : metric_space (α × β) :=
 lemma prod.dist_eq [metric_space β] {x y : α × β} :
   dist x y = max (dist x.1 y.1) (dist x.2 y.2) := rfl
 
+theorem ball_prod_same [metric_space β] (x : α) (y : β) (r : ℝ) :
+  (ball x r).prod (ball y r) = ball (x, y) r :=
+ext $ λ z, by simp [prod.dist_eq]
+
+theorem closed_ball_prod_same [metric_space β] (x : α) (y : β) (r : ℝ) :
+  (closed_ball x r).prod (closed_ball y r) = closed_ball (x, y) r :=
+ext $ λ z, by simp [prod.dist_eq]
+
 end prod
 
 theorem uniform_continuous_dist : uniform_continuous (λp:α×α, dist p.1 p.2) :=

src/topology/metric_space/emetric_space.lean

@@ -585,6 +585,14 @@ is_open_iff.2 $ λ y hy, ⟨⊤, ennreal.coe_lt_top, subset_compl_iff_disjoint.2
 theorem ball_mem_nhds (x : α) {ε : ennreal} (ε0 : 0 < ε) : ball x ε ∈ 𝓝 x :=
 mem_nhds_sets is_open_ball (mem_ball_self ε0)
 
+theorem ball_prod_same [emetric_space β] (x : α) (y : β) (r : ennreal) :
+  (ball x r).prod (ball y r) = ball (x, y) r :=
+ext $ λ z, max_lt_iff.symm
+
+theorem closed_ball_prod_same [emetric_space β] (x : α) (y : β) (r : ennreal) :
+  (closed_ball x r).prod (closed_ball y r) = closed_ball (x, y) r :=
+ext $ λ z, max_le_iff.symm
+
 /-- ε-characterization of the closure in emetric spaces -/
 theorem mem_closure_iff :
   x ∈ closure s ↔ ∀ε>0, ∃y ∈ s, edist x y < ε :=