refactor(MetricSpace/Basic): use cobounded more (#7543)

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -46,7 +46,7 @@ normed group
 
 variable {𝓕 𝕜 α ι κ E F G : Type*}
 
-open Filter Function Metric
+open Filter Function Metric Bornology
 
 open BigOperators ENNReal Filter NNReal Uniformity Pointwise Topology
 
@@ -409,9 +409,22 @@ theorem Isometry.norm_map_of_map_one {f : E → F} (hi : Isometry f) (h₁ : f 1
 #align isometry.norm_map_of_map_one Isometry.norm_map_of_map_one
 #align isometry.norm_map_of_map_zero Isometry.norm_map_of_map_zero
 
+@[to_additive (attr := simp) comap_norm_atTop]
+theorem comap_norm_atTop' : comap norm atTop = cobounded E := by
+  simpa only [dist_one_right] using comap_dist_right_atTop (1 : E)
+
+@[to_additive (attr := simp) tendsto_norm_atTop_iff_cobounded]
+theorem tendsto_norm_atTop_iff_cobounded' {f : α → E} {l : Filter α} :
+    Tendsto (‖f ·‖) l atTop ↔ Tendsto f l (cobounded E) := by
+  rw [← comap_norm_atTop', tendsto_comap_iff]; rfl
+
+@[to_additive tendsto_norm_cobounded_atTop]
+theorem tendsto_norm_cobounded_atTop' : Tendsto norm (cobounded E) atTop :=
+  tendsto_norm_atTop_iff_cobounded'.2 tendsto_id
+
 @[to_additive tendsto_norm_cocompact_atTop]
-theorem tendsto_norm_cocompact_atTop' [ProperSpace E] : Tendsto norm (cocompact E) atTop := by
-  simpa only [dist_one_right] using tendsto_dist_right_cocompact_atTop (1 : E)
+theorem tendsto_norm_cocompact_atTop' [ProperSpace E] : Tendsto norm (cocompact E) atTop :=
+  cobounded_eq_cocompact (α := E) ▸ tendsto_norm_cobounded_atTop'
 #align tendsto_norm_cocompact_at_top' tendsto_norm_cocompact_atTop'
 #align tendsto_norm_cocompact_at_top tendsto_norm_cocompact_atTop
 

Mathlib/Topology/Bornology/Basic.lean

@@ -335,6 +335,11 @@ class BoundedSpace (α : Type*) [Bornology α] : Prop where
   bounded_univ : Bornology.IsBounded (univ : Set α)
 #align bounded_space BoundedSpace
 
+/-- A finite space is bounded. -/
+instance (priority := 100) BoundedSpace.of_finite {α : Type*} [Bornology α] [Finite α] :
+    BoundedSpace α where
+  bounded_univ := (toFinite _).isBounded
+
 namespace Bornology
 
 variable [Bornology α]

Mathlib/Topology/Instances/Int.lean

@@ -70,9 +70,13 @@ instance : ProperSpace ℤ :=
     exact (Set.finite_Icc _ _).isCompact⟩
 
 @[simp]
-theorem cocompact_eq : cocompact ℤ = atBot ⊔ atTop := by
-  simp_rw [← comap_dist_right_atTop_eq_cocompact (0 : ℤ), dist_eq', sub_zero,
+theorem cobounded_eq : Bornology.cobounded ℤ = atBot ⊔ atTop := by
+  simp_rw [← comap_dist_right_atTop (0 : ℤ), dist_eq', sub_zero,
     ← comap_abs_atTop, ← @Int.comap_cast_atTop ℝ, comap_comap]; rfl
+
+@[simp]
+theorem cocompact_eq : cocompact ℤ = atBot ⊔ atTop := by
+  rw [← cobounded_eq_cocompact, cobounded_eq]
 #align int.cocompact_eq Int.cocompact_eq
 
 @[simp]

Mathlib/Topology/Instances/Real.lean

@@ -77,10 +77,13 @@ theorem Real.isTopologicalBasis_Ioo_rat :
       h ⟨hlq.trans hqa', ha'p.trans hpu⟩⟩
 #align real.is_topological_basis_Ioo_rat Real.isTopologicalBasis_Ioo_rat
 
+@[simp]
+theorem Real.cobounded_eq : cobounded ℝ = atBot ⊔ atTop := by
+  simp only [← comap_dist_right_atTop (0 : ℝ), Real.dist_eq, sub_zero, comap_abs_atTop]
+
 @[simp]
 theorem Real.cocompact_eq : cocompact ℝ = atBot ⊔ atTop := by
-  simp only [← comap_dist_right_atTop_eq_cocompact (0 : ℝ), Real.dist_eq, sub_zero,
-    comap_abs_atTop]
+  rw [← cobounded_eq_cocompact, cobounded_eq]
 #align real.cocompact_eq Real.cocompact_eq
 
 /- TODO(Mario): Prove that these are uniform isomorphisms instead of uniform embeddings

Mathlib/Topology/MetricSpace/Basic.lean

@@ -2224,17 +2224,6 @@ instance (priority := 100) secondCountable_of_proper [ProperSpace α] :
   · exact ⟨⟨fun _ => ∅, fun _ => isCompact_empty, iUnion_eq_univ_iff.2 fun x => (hn ⟨x⟩).elim⟩⟩
 #align second_countable_of_proper secondCountable_of_proper
 
-theorem tendsto_dist_right_cocompact_atTop [ProperSpace α] (x : α) :
-    Tendsto (fun y => dist y x) (cocompact α) atTop :=
-  (hasBasis_cocompact.tendsto_iff atTop_basis).2 fun r _ =>
-    ⟨closedBall x r, isCompact_closedBall x r, fun _y hy => (not_le.1 <| mt mem_closedBall.2 hy).le⟩
-#align tendsto_dist_right_cocompact_at_top tendsto_dist_right_cocompact_atTop
-
-theorem tendsto_dist_left_cocompact_atTop [ProperSpace α] (x : α) :
-    Tendsto (dist x) (cocompact α) atTop := by
-  simpa only [dist_comm] using tendsto_dist_right_cocompact_atTop x
-#align tendsto_dist_left_cocompact_at_top tendsto_dist_left_cocompact_atTop
-
 /-- If all closed balls of large enough radius are compact, then the space is proper. Especially
 useful when the lower bound for the radius is 0. -/
 theorem properSpace_of_compact_closedBall_of_le (R : ℝ)
@@ -2408,6 +2397,9 @@ theorem _root_.Bornology.IsBounded.subset_ball_lt (h : IsBounded s) (a : ℝ) (c
 theorem _root_.Bornology.IsBounded.subset_ball (h : IsBounded s) (c : α) : ∃ r, s ⊆ ball c r :=
   (h.subset_ball_lt 0 c).imp fun _ ↦ And.right
 
+theorem isBounded_iff_subset_ball (c : α) : IsBounded s ↔ ∃ r, s ⊆ ball c r :=
+  ⟨(IsBounded.subset_ball · c), fun ⟨_r, hr⟩ ↦ isBounded_ball.subset hr⟩
+
 theorem _root_.Bornology.IsBounded.subset_closedBall_lt (h : IsBounded s) (a : ℝ) (c : α) :
     ∃ r, a < r ∧ s ⊆ closedBall c r :=
   let ⟨r, har, hr⟩ := h.subset_ball_lt a c
@@ -2434,6 +2426,39 @@ theorem isBounded_closure_iff : IsBounded (closure s) ↔ IsBounded s :=
 #align metric.bounded_bUnion Bornology.isBounded_biUnion
 #align metric.bounded.prod Bornology.IsBounded.prod
 
+theorem hasBasis_cobounded_compl_closedBall (c : α) :
+    (cobounded α).HasBasis (fun _ ↦ True) (fun r ↦ (closedBall c r)ᶜ) :=
+  ⟨compl_surjective.forall.2 fun _ ↦ (isBounded_iff_subset_closedBall c).trans <| by simp⟩
+
+theorem hasBasis_cobounded_compl_ball (c : α) :
+    (cobounded α).HasBasis (fun _ ↦ True) (fun r ↦ (ball c r)ᶜ) :=
+  ⟨compl_surjective.forall.2 fun _ ↦ (isBounded_iff_subset_ball c).trans <| by simp⟩
+
+@[simp]
+theorem comap_dist_right_atTop (c : α) : comap (dist · c) atTop = cobounded α :=
+  (atTop_basis.comap _).eq_of_same_basis <| by
+    simpa only [compl_def, mem_ball, not_lt] using hasBasis_cobounded_compl_ball c
+
+@[simp]
+theorem comap_dist_left_atTop (c : α) : comap (dist c) atTop = cobounded α := by
+  simpa only [dist_comm _ c] using comap_dist_right_atTop c
+
+@[simp]
+theorem tendsto_dist_right_atTop_iff (c : α) {f : β → α} {l : Filter β} :
+    Tendsto (fun x ↦ dist (f x) c) l atTop ↔ Tendsto f l (cobounded α) := by
+  rw [← comap_dist_right_atTop c, tendsto_comap_iff]; rfl
+
+@[simp]
+theorem tendsto_dist_left_atTop_iff (c : α) {f : β → α} {l : Filter β} :
+    Tendsto (fun x ↦ dist c (f x)) l atTop ↔ Tendsto f l (cobounded α) := by
+  simp only [dist_comm c, tendsto_dist_right_atTop_iff]
+
+theorem tendsto_dist_right_cobounded_atTop (c : α) : Tendsto (dist · c) (cobounded α) atTop :=
+  tendsto_iff_comap.2 (comap_dist_right_atTop c).ge
+
+theorem tendsto_dist_left_cobounded_atTop (c : α) : Tendsto (dist c) (cobounded α) atTop :=
+  tendsto_iff_comap.2 (comap_dist_left_atTop c).ge
+
 /-- A totally bounded set is bounded -/
 theorem _root_.TotallyBounded.isBounded {s : Set α} (h : TotallyBounded s) : IsBounded s :=
   -- We cover the totally bounded set by finitely many balls of radius 1,
@@ -2452,6 +2477,11 @@ theorem _root_.IsCompact.isBounded {s : Set α} (h : IsCompact s) : IsBounded s
 #align set.finite.bounded Set.Finite.isBounded
 #align metric.bounded_singleton Bornology.isBounded_singleton
 
+theorem cobounded_le_cocompact : cobounded α ≤ cocompact α :=
+  hasBasis_cocompact.ge_iff.2 fun _s hs ↦ hs.isBounded
+#align comap_dist_right_at_top_le_cocompact Metric.cobounded_le_cocompactₓ
+#align comap_dist_left_at_top_le_cocompact Metric.cobounded_le_cocompactₓ
+
 /-- Characterization of the boundedness of the range of a function -/
 theorem isBounded_range_iff {f : β → α} : IsBounded (range f) ↔ ∃ C, ∀ x y, dist (f x) (f y) ≤ C :=
   isBounded_iff.trans <| by simp only [forall_range_iff]
@@ -2833,32 +2863,29 @@ def evalDiam : PositivityExt where eval {_ _} _zα _pα e := do
 
 end Mathlib.Meta.Positivity
 
-theorem comap_dist_right_atTop_le_cocompact (x : α) :
-    comap (fun y => dist y x) atTop ≤ cocompact α := by
-  refine' Filter.hasBasis_cocompact.ge_iff.2 fun s hs => mem_comap.2 _
-  rcases hs.isBounded.subset_closedBall x with ⟨r, hr⟩
-  exact ⟨Ioi r, Ioi_mem_atTop r, fun y hy hys => (mem_closedBall.1 <| hr hys).not_lt hy⟩
-#align comap_dist_right_at_top_le_cocompact comap_dist_right_atTop_le_cocompact
+theorem Metric.cobounded_eq_cocompact [ProperSpace α] : cobounded α = cocompact α := by
+  nontriviality α; inhabit α
+  exact cobounded_le_cocompact.antisymm <| (hasBasis_cobounded_compl_closedBall default).ge_iff.2
+    fun _ _ ↦ (isCompact_closedBall _ _).compl_mem_cocompact
+#align comap_dist_right_at_top_eq_cocompact Metric.cobounded_eq_cocompact
 
-theorem comap_dist_left_atTop_le_cocompact (x : α) : comap (dist x) atTop ≤ cocompact α := by
-  simpa only [dist_comm _ x] using comap_dist_right_atTop_le_cocompact x
-#align comap_dist_left_at_top_le_cocompact comap_dist_left_atTop_le_cocompact
+theorem tendsto_dist_right_cocompact_atTop [ProperSpace α] (x : α) :
+    Tendsto (dist · x) (cocompact α) atTop :=
+  (tendsto_dist_right_cobounded_atTop x).mono_left cobounded_eq_cocompact.ge
+#align tendsto_dist_right_cocompact_at_top tendsto_dist_right_cocompact_atTop
 
-theorem comap_dist_right_atTop_eq_cocompact [ProperSpace α] (x : α) :
-    comap (fun y => dist y x) atTop = cocompact α :=
-  (comap_dist_right_atTop_le_cocompact x).antisymm <|
-    (tendsto_dist_right_cocompact_atTop x).le_comap
-#align comap_dist_right_at_top_eq_cocompact comap_dist_right_atTop_eq_cocompact
+theorem tendsto_dist_left_cocompact_atTop [ProperSpace α] (x : α) :
+    Tendsto (dist x) (cocompact α) atTop :=
+  (tendsto_dist_left_cobounded_atTop x).mono_left cobounded_eq_cocompact.ge
+#align tendsto_dist_left_cocompact_at_top tendsto_dist_left_cocompact_atTop
 
 theorem comap_dist_left_atTop_eq_cocompact [ProperSpace α] (x : α) :
-    comap (dist x) atTop = cocompact α :=
-  (comap_dist_left_atTop_le_cocompact x).antisymm <| (tendsto_dist_left_cocompact_atTop x).le_comap
+    comap (dist x) atTop = cocompact α := by simp [cobounded_eq_cocompact]
 #align comap_dist_left_at_top_eq_cocompact comap_dist_left_atTop_eq_cocompact
 
 theorem tendsto_cocompact_of_tendsto_dist_comp_atTop {f : β → α} {l : Filter β} (x : α)
-    (h : Tendsto (fun y => dist (f y) x) l atTop) : Tendsto f l (cocompact α) := by
-  refine' Tendsto.mono_right _ (comap_dist_right_atTop_le_cocompact x)
-  rwa [tendsto_comap_iff]
+    (h : Tendsto (fun y => dist (f y) x) l atTop) : Tendsto f l (cocompact α) :=
+  ((tendsto_dist_right_atTop_iff _).1 h).mono_right cobounded_le_cocompact
 #align tendsto_cocompact_of_tendsto_dist_comp_at_top tendsto_cocompact_of_tendsto_dist_comp_atTop
 
 /-- We now define `MetricSpace`, extending `PseudoMetricSpace`. -/