diff --git a/src/topology/continuous_function/bounded.lean b/src/topology/continuous_function/bounded.lean index d2fe2e5e2cd2b..4e6f90cab2e36 100644 --- a/src/topology/continuous_function/bounded.lean +++ b/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 := diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean index 784216823c92b..829fe70268076 100644 --- a/src/topology/metric_space/basic.lean +++ b/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 diff --git a/src/topology/metric_space/closeds.lean b/src/topology/metric_space/closeds.lean index 77a2002d81514..dcbfb77ea0c57 100644 --- a/src/topology/metric_space/closeds.lean +++ b/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 α} : diff --git a/src/topology/metric_space/gromov_hausdorff_realized.lean b/src/topology/metric_space/gromov_hausdorff_realized.lean index 20417005f6676..cc1860ca7f028 100644 --- a/src/topology/metric_space/gromov_hausdorff_realized.lean +++ b/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