feat: bounded distance implies bounded space (#31555)

Author: EtienneC30

Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

@@ -594,6 +594,10 @@ theorem isBounded_iff {s : Set α} :
   rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_setOf_eq,
     compl_compl]
 
+lemma boundedSpace_iff : BoundedSpace α ↔ ∃ C, ∀ a b : α, dist a b ≤ C := by
+  rw [← isBounded_univ, Metric.isBounded_iff]
+  simp
+
 theorem isBounded_iff_eventually {s : Set α} :
     IsBounded s ↔ ∀ᶠ C in atTop, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C :=
   isBounded_iff.trans
@@ -610,6 +614,13 @@ theorem isBounded_iff_nndist {s : Set α} :
   simp only [isBounded_iff_exists_ge 0, NNReal.exists, ← NNReal.coe_le_coe, ← dist_nndist,
     NNReal.coe_mk, exists_prop]
 
+lemma boundedSpace_iff_nndist : BoundedSpace α ↔ ∃ C, ∀ a b : α, nndist a b ≤ C := by
+  rw [← isBounded_univ, Metric.isBounded_iff_nndist]
+  simp
+
+lemma boundedSpace_iff_edist : BoundedSpace α ↔ ∃ C : ℝ≥0, ∀ a b : α, edist a b ≤ C := by
+  simp [Metric.boundedSpace_iff_nndist]
+
 theorem toUniformSpace_eq :
     ‹PseudoMetricSpace α›.toUniformSpace = .ofDist dist dist_self dist_comm dist_triangle :=
   UniformSpace.ext PseudoMetricSpace.uniformity_dist