feat: totally bounded sets have finite covers (#31537)

New result: a totally bounded set has finite `ε`-covers for all `ε > 0`.
I then use it to golf and generalize `exists_finite_isCover_of_isCompact_closure` and `exists_finite_isCover_of_isCompact` to extended pseudo-metric spaces.

Co-authored-by: Remy Degenne <remydegenne@gmail.com>

Author: RemyDegenne

Mathlib/Data/Rel/Cover.lean

@@ -44,6 +44,11 @@ def IsCover (U : SetRel X X) (s N : Set X) : Prop := ∀ ⦃x⦄, x ∈ s → 
 protected nonrec lemma IsCover.nonempty (hsN : IsCover U s N) (hs : s.Nonempty) : N.Nonempty :=
   let ⟨_x, hx⟩ := hs; let ⟨y, hy, _⟩ := hsN hx; ⟨y, hy⟩
 
+@[simp] lemma IsCover.refl (U : SetRel X X) [U.IsRefl] (s : Set X) : IsCover U s s :=
+  fun a ha ↦ ⟨a, ha, U.rfl⟩
+
+lemma IsCover.rfl {U : SetRel X X} [U.IsRefl] {s : Set X} : IsCover U s s := refl U s
+
 @[simp] protected lemma isCover_univ : IsCover univ s N ↔ (s.Nonempty → N.Nonempty) := by
   simp [IsCover, Set.Nonempty]
 

Mathlib/Topology/MetricSpace/Cover.lean

@@ -45,16 +45,25 @@ def IsCover (ε : ℝ≥0) (s N : Set X) : Prop := SetRel.IsCover {(x, y) | edis
 
 @[simp] protected nonrec lemma IsCover.empty : IsCover ε ∅ N := .empty
 
+@[simp] lemma isCover_empty_right : IsCover ε s ∅ ↔ s = ∅ := SetRel.isCover_empty_right
+
 protected nonrec lemma IsCover.nonempty (hsN : IsCover ε s N) (hs : s.Nonempty) : N.Nonempty :=
   hsN.nonempty hs
 
+@[simp] lemma IsCover.refl (ε : ℝ≥0) (s : Set X) : IsCover ε s s := .rfl
+lemma IsCover.rfl {ε : ℝ≥0} {s : Set X} : IsCover ε s s := refl ε s
+
 nonrec lemma IsCover.mono (hN : N₁ ⊆ N₂) (h₁ : IsCover ε s N₁) : IsCover ε s N₂ := h₁.mono hN
 
 nonrec lemma IsCover.anti (hst : s ⊆ t) (ht : IsCover ε t N) : IsCover ε s N := ht.anti hst
 
 lemma IsCover.mono_radius (hεδ : ε ≤ δ) (hε : IsCover ε s N) : IsCover δ s N :=
   hε.mono_entourage fun xy hxy ↦ by dsimp at *; exact le_trans hxy <| mod_cast hεδ
 
+lemma IsCover.singleton_of_ediam_le (hA : EMetric.diam s ≤ ε) (hx : x ∈ s) :
+    IsCover ε s ({x} : Set X) :=
+  fun _ h_mem ↦ ⟨x, by simp, (EMetric.edist_le_diam_of_mem h_mem hx).trans hA⟩
+
 lemma isCover_iff_subset_iUnion_emetricClosedBall :
     IsCover ε s N ↔ s ⊆ ⋃ y ∈ N, EMetric.closedBall y ε := by
   simp [IsCover, SetRel.IsCover, subset_def]
@@ -66,6 +75,28 @@ nonrec lemma IsCover.of_maximal_isSeparated (hN : Maximal (fun N ↦ N ⊆ s ∧
     IsCover ε s N :=
   .of_maximal_isSeparated <| by simpa [isSeparated_iff_setRelIsSeparated] using hN
 
+/-- A totally bounded set has finite `ε`-covers for all `ε > 0`. -/
+lemma exists_finite_isCover_of_totallyBounded (hε : ε ≠ 0) (hs : TotallyBounded s) :
+    ∃ N ⊆ s, N.Finite ∧ IsCover ε s N := by
+  rw [EMetric.totallyBounded_iff'] at hs
+  obtain ⟨N, hNA, hN_finite, hN⟩ := hs ε (mod_cast hε.bot_lt)
+  simp only [isCover_iff_subset_iUnion_emetricClosedBall]
+  refine ⟨N, by simpa, by simpa, ?_⟩
+  · refine hN.trans fun x hx ↦ ?_
+    simp only [Set.mem_iUnion, EMetric.mem_ball, exists_prop, EMetric.mem_closedBall] at hx ⊢
+    obtain ⟨y, hyN, hy⟩ := hx
+    exact ⟨y, hyN, hy.le⟩
+
+/-- A relatively compact set admits a finite cover. -/
+lemma exists_finite_isCover_of_isCompact_closure (hε : ε ≠ 0) (hs : IsCompact (closure s)) :
+    ∃ N ⊆ s, N.Finite ∧ IsCover ε s N :=
+  exists_finite_isCover_of_totallyBounded hε (hs.totallyBounded.subset subset_closure)
+
+/-- A compact set admits a finite cover. -/
+lemma exists_finite_isCover_of_isCompact (hε : ε ≠ 0) (hs : IsCompact s) :
+    ∃ N ⊆ s, N.Finite ∧ IsCover ε s N :=
+  exists_finite_isCover_of_totallyBounded hε hs.totallyBounded
+
 end PseudoEMetricSpace
 
 section PseudoMetricSpace
@@ -77,23 +108,6 @@ lemma isCover_iff_subset_iUnion_closedBall : IsCover ε s N ↔ s ⊆ ⋃ y ∈
 alias ⟨IsCover.subset_iUnion_closedBall, IsCover.of_subset_iUnion_closedBall⟩ :=
   isCover_iff_subset_iUnion_closedBall
 
-/-- A relatively compact set admits a finite cover. -/
-lemma exists_finite_isCover_of_isCompact_closure (hε : ε ≠ 0) (hs : IsCompact (closure s)) :
-    ∃ N ⊆ s, N.Finite ∧ IsCover ε s N := by
-  obtain ⟨N, hNs, hN, hsN⟩ :=
-    exists_finite_cover_balls_of_isCompact_closure hs (ε := ε) (by positivity)
-  refine ⟨N, hNs, hN, .of_subset_iUnion_closedBall <| hsN.trans ?_⟩
-  gcongr
-  exact ball_subset_closedBall
-
-/-- A compact set admits a finite cover. -/
-lemma exists_finite_isCover_of_isCompact (hε : ε ≠ 0) (hs : IsCompact s) :
-    ∃ N ⊆ s, N.Finite ∧ IsCover ε s N := by
-  obtain ⟨N, hNs, hN, hsN⟩ := hs.finite_cover_balls (e := ε) (by positivity)
-  refine ⟨N, hNs, hN, .of_subset_iUnion_closedBall <| hsN.trans ?_⟩
-  gcongr
-  exact ball_subset_closedBall
-
 lemma IsCover.of_subset_cthickening_of_lt {δ : ℝ≥0} (hsN : s ⊆ cthickening ε N) (hεδ : ε < δ) :
     IsCover δ s N :=
   .of_subset_iUnion_closedBall <| hsN.trans (cthickening_subset_iUnion_closedBall_of_lt _