feat(topology/metric_space/basic): an order-bounded set is metric-bou…

…nded (#8335)

src/topology/continuous_function/bounded.lean

@@ -59,7 +59,7 @@ rfl
 
 /-- A continuous function on a compact space is automatically a bounded continuous function. -/
 def mk_of_compact [compact_space α] (f : C(α, β)) : α →ᵇ β :=
-⟨f, bounded_range_iff.1 $ bounded_of_compact $ is_compact_range f.continuous⟩
+⟨f, bounded_range_iff.1 (is_compact_range f.continuous).bounded⟩
 
 @[simp] lemma mk_of_compact_apply [compact_space α] (f : C(α, β)) (a : α) :
   mk_of_compact f a = f a :=

src/topology/metric_space/basic.lean

@@ -1561,14 +1561,17 @@ lemma bounded_bUnion {I : set β} {s : β → set α} (H : finite I) :
 finite.induction_on H (by simp) $ λ x I _ _ IH,
 by simp [or_imp_distrib, forall_and_distrib, IH]
 
-/-- A compact set is bounded -/
-lemma bounded_of_compact {s : set α} (h : is_compact s) : bounded s :=
--- We cover the compact set by finitely many balls of radius 1,
+/-- A totally bounded set is bounded -/
+lemma _root_.totally_bounded.bounded {s : set α} (h : totally_bounded s) : bounded s :=
+-- We cover the totally bounded set by finitely many balls of radius 1,
 -- and then argue that a finite union of bounded sets is bounded
-let ⟨t, ht, fint, subs⟩ := finite_cover_balls_of_compact h zero_lt_one in
+let ⟨t, fint, subs⟩ := (totally_bounded_iff.mp h) 1 zero_lt_one in
 bounded.subset subs $ (bounded_bUnion fint).2 $ λ i hi, bounded_ball
 
-alias bounded_of_compact ← is_compact.bounded
+/-- A compact set is bounded -/
+lemma _root_.is_compact.bounded {s : set α} (h : is_compact s) : bounded s :=
+-- A compact set is totally bounded, thus bounded
+h.totally_bounded.bounded
 
 /-- A finite set is bounded -/
 lemma bounded_of_finite {s : set α} (h : finite s) : bounded s :=
@@ -1602,6 +1605,31 @@ lemma compact_iff_closed_bounded [t2_space α] [proper_space α] :
   exact compact_of_is_closed_subset (proper_space.compact_ball x r) hc hr
 end⟩
 
+section conditionally_complete_linear_order
+
+variables [conditionally_complete_linear_order α] [order_topology α]
+
+lemma bounded_Icc (a b : α) : bounded (Icc a b) :=
+(totally_bounded_Icc a b).bounded
+
+lemma bounded_Ico (a b : α) : bounded (Ico a b) :=
+(totally_bounded_Ico a b).bounded
+
+lemma bounded_Ioc (a b : α) : bounded (Ioc a b) :=
+(totally_bounded_Ioc a b).bounded
+
+lemma bounded_Ioo (a b : α) : bounded (Ioo a b) :=
+(totally_bounded_Ioo a b).bounded
+
+/-- In a pseudo metric space with a conditionally complete linear order such that the order and the
+    metric structure give the same topology, any order-bounded set is metric-bounded. -/
+lemma bounded_of_bdd_above_of_bdd_below {s : set α} (h₁ : bdd_above s) (h₂ : bdd_below s) :
+  bounded s :=
+let ⟨u, hu⟩ := h₁, ⟨l, hl⟩ := h₂ in
+bounded.subset (λ x hx, mem_Icc.mpr ⟨hl hx, hu hx⟩) (bounded_Icc l u)
+
+end conditionally_complete_linear_order
+
 end bounded
 
 section diam

src/topology/metric_space/closeds.lean

@@ -392,7 +392,7 @@ variables {α : Type u} [metric_space α]
 edistance between two such sets is finite. -/
 instance nonempty_compacts.metric_space : metric_space (nonempty_compacts α) :=
 emetric_space.to_metric_space $ λx y, Hausdorff_edist_ne_top_of_nonempty_of_bounded x.2.1 y.2.1
-  (bounded_of_compact x.2.2) (bounded_of_compact y.2.2)
+  x.2.2.bounded y.2.2.bounded
 
 /-- The distance on `nonempty_compacts α` is the Hausdorff distance, by construction -/
 lemma nonempty_compacts.dist_eq {x y : nonempty_compacts α} :

src/topology/metric_space/gromov_hausdorff_realized.lean

@@ -89,7 +89,7 @@ local attribute [instance, priority 10] inhabited_of_nonempty'
 
 private lemma max_var_bound : dist x y ≤ max_var X Y := calc
   dist x y ≤ diam (univ : set (X ⊕ Y)) :
-    dist_le_diam_of_mem (bounded_of_compact compact_univ) (mem_univ _) (mem_univ _)
+    dist_le_diam_of_mem bounded_of_compact_space (mem_univ _) (mem_univ _)
   ... = diam (inl '' (univ : set X) ∪ inr '' (univ : set Y)) :
     by apply congr_arg; ext x y z; cases x; simp [mem_univ, mem_range_self]
   ... ≤ diam (inl '' (univ : set X)) + dist (inl (default X)) (inr (default Y)) +
@@ -328,10 +328,10 @@ begin
       ... ≤ diam (univ : set X) + 1 + diam (univ : set Y) :
       begin
         apply add_le_add (add_le_add _ (le_refl _)),
-        exact dist_le_diam_of_mem (bounded_of_compact (compact_univ)) (mem_univ _) (mem_univ _),
+        exact dist_le_diam_of_mem bounded_of_compact_space (mem_univ _) (mem_univ _),
         any_goals { exact ordered_add_comm_monoid.to_covariant_class_left ℝ },
         any_goals { exact ordered_add_comm_monoid.to_covariant_class_right ℝ },
-        exact dist_le_diam_of_mem (bounded_of_compact (compact_univ)) (mem_univ _) (mem_univ _),
+        exact dist_le_diam_of_mem bounded_of_compact_space (mem_univ _) (mem_univ _),
       end,
     exact le_trans A B },
   { have A : (⨅ x, candidates_b_dist X Y (inl x, inr y)) ≤
@@ -342,10 +342,10 @@ begin
       ... ≤ diam (univ : set X) + 1 + diam (univ : set Y) :
       begin
         apply add_le_add (add_le_add _ (le_refl _)),
-        exact dist_le_diam_of_mem (bounded_of_compact (compact_univ)) (mem_univ _) (mem_univ _),
+        exact dist_le_diam_of_mem bounded_of_compact_space (mem_univ _) (mem_univ _),
         any_goals { exact ordered_add_comm_monoid.to_covariant_class_left ℝ },
         any_goals { exact ordered_add_comm_monoid.to_covariant_class_right ℝ },
-        exact dist_le_diam_of_mem (bounded_of_compact (compact_univ)) (mem_univ _) (mem_univ _)
+        exact dist_le_diam_of_mem bounded_of_compact_space (mem_univ _) (mem_univ _)
       end,
     exact le_trans A B },
 end