feat(UniformSpace/Cauchy): add lemmas about TotallyBounded (#13451)

Author: urkud

Mathlib/Data/Set/Finite.lean

@@ -1038,6 +1038,13 @@ theorem Finite.finite_subsets {α : Type u} {a : Set α} (h : a.Finite) : { b |
 protected theorem Finite.powerset {s : Set α} (h : s.Finite) : (𝒫 s).Finite :=
   h.finite_subsets
 
+theorem exists_subset_image_finite_and {f : α → β} {s : Set α} {p : Set β → Prop} :
+    (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t) := by
+  classical
+  simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
+    Finset.subset_image_iff]
+  aesop
+
 section Pi
 variable {ι : Type*} [Finite ι] {κ : ι → Type*} {t : ∀ i, Set (κ i)}
 

Mathlib/Topology/Instances/Rat.lean

@@ -113,8 +113,9 @@ instance : TopologicalRing ℚ := inferInstance
 #align rat.continuous_mul continuous_mul
 
 nonrec theorem totallyBounded_Icc (a b : ℚ) : TotallyBounded (Icc a b) := by
-  simpa only [preimage_cast_Icc] using
-    totallyBounded_preimage Rat.uniformEmbedding_coe_real (totallyBounded_Icc (a : ℝ) b)
+  simpa only [preimage_cast_Icc]
+    using totallyBounded_preimage Rat.uniformEmbedding_coe_real.toUniformInducing
+      (totallyBounded_Icc (a : ℝ) b)
 #align rat.totally_bounded_Icc Rat.totallyBounded_Icc
 
 end Rat

Mathlib/Topology/MetricSpace/Bounded.lean

@@ -339,15 +339,15 @@ theorem _root_.totallyBounded_Icc (a b : α) : TotallyBounded (Icc a b) :=
 #align totally_bounded_Icc totallyBounded_Icc
 
 theorem _root_.totallyBounded_Ico (a b : α) : TotallyBounded (Ico a b) :=
-  totallyBounded_subset Ico_subset_Icc_self (totallyBounded_Icc a b)
+  (totallyBounded_Icc a b).subset Ico_subset_Icc_self
 #align totally_bounded_Ico totallyBounded_Ico
 
 theorem _root_.totallyBounded_Ioc (a b : α) : TotallyBounded (Ioc a b) :=
-  totallyBounded_subset Ioc_subset_Icc_self (totallyBounded_Icc a b)
+  (totallyBounded_Icc a b).subset Ioc_subset_Icc_self
 #align totally_bounded_Ioc totallyBounded_Ioc
 
 theorem _root_.totallyBounded_Ioo (a b : α) : TotallyBounded (Ioo a b) :=
-  totallyBounded_subset Ioo_subset_Icc_self (totallyBounded_Icc a b)
+  (totallyBounded_Icc a b).subset Ioo_subset_Icc_self
 #align totally_bounded_Ioo totallyBounded_Ioo
 
 theorem isBounded_Icc (a b : α) : IsBounded (Icc a b) :=

Mathlib/Topology/UniformSpace/Cauchy.lean

@@ -533,9 +533,7 @@ theorem TotallyBounded.exists_subset {s : Set α} (hs : TotallyBounded s) {U : S
 theorem totallyBounded_iff_subset {s : Set α} :
     TotallyBounded s ↔
       ∀ d ∈ 𝓤 α, ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, { x | (x, y) ∈ d } :=
-  ⟨fun H _ hd => H.exists_subset hd, fun H d hd =>
-    let ⟨t, _, ht⟩ := H d hd
-    ⟨t, ht⟩⟩
+  ⟨fun H _ hd ↦ H.exists_subset hd, fun H d hd ↦ let ⟨t, _, ht⟩ := H d hd; ⟨t, ht⟩⟩
 #align totally_bounded_iff_subset totallyBounded_iff_subset
 
 theorem Filter.HasBasis.totallyBounded_iff {ι} {p : ι → Prop} {U : ι → Set (α × α)}
@@ -552,15 +550,14 @@ theorem totallyBounded_of_forall_symm {s : Set α}
     simpa only [ball_eq_of_symmetry hV.2] using h V hV.1 hV.2
 #align totally_bounded_of_forall_symm totallyBounded_of_forall_symm
 
-theorem totallyBounded_subset {s₁ s₂ : Set α} (hs : s₁ ⊆ s₂) (h : TotallyBounded s₂) :
+theorem TotallyBounded.subset {s₁ s₂ : Set α} (hs : s₁ ⊆ s₂) (h : TotallyBounded s₂) :
     TotallyBounded s₁ := fun d hd =>
   let ⟨t, ht₁, ht₂⟩ := h d hd
   ⟨t, ht₁, Subset.trans hs ht₂⟩
-#align totally_bounded_subset totallyBounded_subset
+#align totally_bounded_subset TotallyBounded.subset
 
-theorem totallyBounded_empty : TotallyBounded (∅ : Set α) := fun _ _ =>
-  ⟨∅, finite_empty, empty_subset _⟩
-#align totally_bounded_empty totallyBounded_empty
+@[deprecated (since := "2024-06-01")]
+alias totallyBounded_subset := TotallyBounded.subset
 
 /-- The closure of a totally bounded set is totally bounded. -/
 theorem TotallyBounded.closure {s : Set α} (h : TotallyBounded s) : TotallyBounded (closure s) :=
@@ -571,6 +568,70 @@ theorem TotallyBounded.closure {s : Set α} (h : TotallyBounded s) : TotallyBoun
         htf.isClosed_biUnion fun _ _ => hV.2.preimage (continuous_id.prod_mk continuous_const)⟩
 #align totally_bounded.closure TotallyBounded.closure
 
+@[simp]
+lemma totallyBounded_closure {s : Set α} : TotallyBounded (closure s) ↔ TotallyBounded s :=
+  ⟨fun h ↦ h.subset subset_closure, TotallyBounded.closure⟩
+
+/-- A finite indexed union is totally bounded
+if and only if each set of the family is totally bounded. -/
+@[simp]
+lemma totallyBounded_iUnion {ι : Sort*} [Finite ι] {s : ι → Set α} :
+    TotallyBounded (⋃ i, s i) ↔ ∀ i, TotallyBounded (s i) := by
+  refine ⟨fun h i ↦ h.subset (subset_iUnion _ _), fun h U hU ↦ ?_⟩
+  choose t htf ht using (h · U hU)
+  refine ⟨⋃ i, t i, finite_iUnion htf, ?_⟩
+  rw [biUnion_iUnion]
+  gcongr; apply ht
+
+/-- A union indexed by a finite set is totally bounded
+if and only if each set of the family is totally bounded. -/
+lemma totallyBounded_biUnion {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set α} :
+    TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i) := by
+  have := hI.to_subtype
+  rw [biUnion_eq_iUnion, totallyBounded_iUnion, Subtype.forall]
+
+/-- A union of a finite family of sets is totally bounded
+if and only if each set of the family is totally bounded. -/
+lemma totallyBounded_sUnion {S : Set (Set α)} (hS : S.Finite) :
+    TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s := by
+  rw [sUnion_eq_biUnion, totallyBounded_biUnion hS]
+
+/-- A finite set is totally bounded. -/
+lemma Set.Finite.totallyBounded {s : Set α} (hs : s.Finite) : TotallyBounded s := fun _U hU ↦
+  ⟨s, hs, fun _x hx ↦ mem_biUnion hx <| refl_mem_uniformity hU⟩
+
+/-- A subsingleton is totally bounded. -/
+lemma Set.Subsingleton.totallyBounded {s : Set α} (hs : s.Subsingleton) :
+    TotallyBounded s :=
+  hs.finite.totallyBounded
+
+@[simp]
+lemma totallyBounded_singleton (a : α) : TotallyBounded {a} := (finite_singleton a).totallyBounded
+
+@[simp]
+theorem totallyBounded_empty : TotallyBounded (∅ : Set α) := finite_empty.totallyBounded
+#align totally_bounded_empty totallyBounded_empty
+
+/-- The union of two sets is totally bounded
+if and only if each of the two sets is totally bounded.-/
+@[simp]
+lemma totallyBounded_union {s t : Set α} :
+    TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t := by
+  rw [union_eq_iUnion, totallyBounded_iUnion]
+  simp [and_comm]
+
+/-- The union of two totally bounded sets is totally bounded. -/
+protected lemma TotallyBounded.union {s t : Set α} (hs : TotallyBounded s) (ht : TotallyBounded t) :
+    TotallyBounded (s ∪ t) :=
+  totallyBounded_union.2 ⟨hs, ht⟩
+
+@[simp]
+lemma totallyBounded_insert (a : α) {s : Set α} :
+    TotallyBounded (insert a s) ↔ TotallyBounded s := by
+  simp_rw [← singleton_union, totallyBounded_union, totallyBounded_singleton, true_and]
+
+protected alias ⟨_, TotallyBounded.insert⟩ := totallyBounded_insert
+
 /-- The image of a totally bounded set under a uniformly continuous map is totally bounded. -/
 theorem TotallyBounded.image [UniformSpace β] {f : α → β} {s : Set α} (hs : TotallyBounded s)
     (hf : UniformContinuous f) : TotallyBounded (f '' s) := fun t ht =>
@@ -662,9 +723,9 @@ theorem isCompact_of_totallyBounded_isClosed [CompleteSpace α] {s : Set α} (ht
 /-- Every Cauchy sequence over `ℕ` is totally bounded. -/
 theorem CauchySeq.totallyBounded_range {s : ℕ → α} (hs : CauchySeq s) :
     TotallyBounded (range s) := by
-  refine totallyBounded_iff_subset.2 fun a ha => ?_
+  intro a ha
   cases' cauchySeq_iff.1 hs a ha with n hn
-  refine ⟨s '' { k | k ≤ n }, image_subset_range _ _, (finite_le_nat _).image _, ?_⟩
+  refine ⟨s '' { k | k ≤ n }, (finite_le_nat _).image _, ?_⟩
   rw [range_subset_iff, biUnion_image]
   intro m
   rw [mem_iUnion₂]

Mathlib/Topology/UniformSpace/UniformEmbedding.lean

@@ -397,17 +397,18 @@ theorem completeSpace_extension {m : β → α} (hm : UniformInducing m) (dense
         ⟩⟩
 #align complete_space_extension completeSpace_extension
 
-theorem totallyBounded_preimage {f : α → β} {s : Set β} (hf : UniformEmbedding f)
-    (hs : TotallyBounded s) : TotallyBounded (f ⁻¹' s) := fun t ht => by
-  rw [← hf.comap_uniformity] at ht
-  rcases mem_comap.2 ht with ⟨t', ht', ts⟩
-  rcases totallyBounded_iff_subset.1 (totallyBounded_subset (image_preimage_subset f s) hs) _ ht'
-    with ⟨c, cs, hfc, hct⟩
-  refine ⟨f ⁻¹' c, hfc.preimage hf.inj.injOn, fun x h => ?_⟩
-  have := hct (mem_image_of_mem f h); simp at this ⊢
-  rcases this with ⟨z, zc, zt⟩
-  rcases cs zc with ⟨y, -, rfl⟩
-  exact ⟨y, zc, ts zt⟩
+lemma totallyBounded_image_iff {f : α → β} {s : Set α} (hf : UniformInducing f) :
+    TotallyBounded (f '' s) ↔ TotallyBounded s := by
+  refine ⟨fun hs ↦ ?_, fun h ↦ h.image hf.uniformContinuous⟩
+  simp_rw [(hf.basis_uniformity (basis_sets _)).totallyBounded_iff]
+  intro t ht
+  rcases exists_subset_image_finite_and.1 (hs.exists_subset ht) with ⟨u, -, hfin, h⟩
+  use u, hfin
+  rwa [biUnion_image, image_subset_iff, preimage_iUnion₂] at h
+
+theorem totallyBounded_preimage {f : α → β} {s : Set β} (hf : UniformInducing f)
+    (hs : TotallyBounded s) : TotallyBounded (f ⁻¹' s) :=
+  (totallyBounded_image_iff hf).1 <| hs.subset <| image_preimage_subset ..
 #align totally_bounded_preimage totallyBounded_preimage
 
 instance CompleteSpace.sum [CompleteSpace α] [CompleteSpace β] : CompleteSpace (Sum α β) := by