feat(Topology/UniformSpace/Closeds): completeness of (Nonempty)Compacts

Mathlib/Topology/MetricSpace/Closeds.lean

@@ -272,13 +272,6 @@ theorem isClosed_in_closeds [CompleteSpace α] :
         _ = ε := ENNReal.add_halves _
     exact mem_biUnion hy this
 
-/-- In a complete space, the type of nonempty compact subsets is complete. This follows
-from the same statement for closed subsets -/
-instance instCompleteSpace [CompleteSpace α] : CompleteSpace (NonemptyCompacts α) :=
-  (completeSpace_iff_isComplete_range
-        isometry_toCloseds.isUniformInducing).2 <|
-    isClosed_in_closeds.isComplete
-
 /-- In a compact space, the type of nonempty compact subsets is compact. This follows from
 the same statement for closed subsets -/
 instance instCompactSpace [CompactSpace α] : CompactSpace (NonemptyCompacts α) :=

Mathlib/Topology/Sets/Compacts.lean

@@ -130,6 +130,13 @@ theorem coe_top [CompactSpace α] : (↑(⊤ : Compacts α) : Set α) = univ :=
 theorem coe_bot : (↑(⊥ : Compacts α) : Set α) = ∅ :=
   rfl
 
+@[simp, norm_cast]
+theorem coe_eq_empty {s : Compacts α} : (s : Set α) = ∅ ↔ s = ⊥ :=
+  SetLike.coe_injective.eq_iff' rfl
+
+theorem coe_nonempty {s : Compacts α} : (s : Set α).Nonempty ↔ s ≠ ⊥ :=
+  nonempty_iff_ne_empty.trans coe_eq_empty.not
+
 @[simp]
 theorem coe_finset_sup {ι : Type*} {s : Finset ι} {f : ι → Compacts α} :
     (↑(s.sup f) : Set α) = s.sup fun i => ↑(f i) := by
@@ -332,6 +339,13 @@ theorem mem_toCompacts {x : α} {s : NonemptyCompacts α} :
 theorem toCompacts_injective : Function.Injective (toCompacts (α := α)) :=
   .of_comp (f := SetLike.coe) SetLike.coe_injective
 
+theorem range_toCompacts : range (toCompacts (α := α)) = {⊥}ᶜ := by
+  ext K
+  rw [mem_compl_singleton_iff, ← Compacts.coe_nonempty]
+  refine ⟨?_, fun h => ⟨⟨K, h⟩, rfl⟩⟩
+  rintro ⟨K, rfl⟩
+  exact K.nonempty
+
 instance : Max (NonemptyCompacts α) :=
   ⟨fun s t => ⟨s.toCompacts ⊔ t.toCompacts, s.nonempty.mono subset_union_left⟩⟩
 

Mathlib/Topology/UniformSpace/Closeds.lean

@@ -9,6 +9,8 @@ public import Mathlib.Topology.Order.Lattice
 public import Mathlib.Topology.Sets.Compacts
 public import Mathlib.Topology.UniformSpace.UniformEmbedding
 
+import Mathlib.Topology.UniformSpace.Compact
+
 /-!
 # Hausdorff uniformity
 
@@ -20,7 +22,7 @@ induced by the Hausdorff metric to hyperspaces of uniform spaces.
 @[expose] public section
 
 open Topology
-open scoped Uniformity
+open scoped Uniformity Filter
 
 variable {α β : Type*}
 
@@ -432,6 +434,53 @@ theorem _root_.IsUniformEmbedding.compacts_map {f : α → β} (hf : IsUniformEm
   __ := hf.isUniformInducing.compacts_map
   injective := map_injective hf.uniformContinuous.continuous hf.injective
 
+instance [CompleteSpace α] : CompleteSpace (Compacts α) := by
+  refine ⟨fun {f} ⟨_, hf⟩ => ?_⟩
+  grw [← Filter.curry_le_prod, (𝓤 α).basis_sets.uniformity_compacts.ge_iff] at hf
+  change ∀ {U} (hU : U ∈ 𝓤 α), ∀ᶠ K in f, ∀ᶠ K' in f, (↑K, ↑K') ∈ hausdorffEntourage U at hf
+  let l : Filter α := f.lift' fun s => ⋃ K ∈ s, K
+  have hl : l.TotallyBounded := by
+    intro U hU
+    obtain ⟨V : SetRel α α, hV, hVU⟩ := comp_mem_uniformity_sets hU
+    obtain ⟨K, hK⟩ := hf (symm_le_uniformity hV) |>.exists
+    obtain ⟨t, ht₁, ht₂⟩ := K.isCompact.totallyBounded V hV
+    rw [← SetRel.preimage_eq_biUnion] at ht₂
+    refine ⟨t, ht₁, Filter.mem_of_superset (Filter.mem_lift' hK) ?_⟩
+    rw [Set.iUnion₂_subset_iff]
+    intro K' ⟨_, (hK' : ↑K' ⊆ V.preimage K)⟩
+    grw [← hVU, SetRel.preimage_comp, ← ht₂, hK']
+  let L : Compacts α := ⟨{x | ClusterPt x l}, hl.isCompact_setOf_clusterPt⟩
+  exists L
+  simp_rw [nhds_eq_comap_uniformity']
+  rw [uniformity_hasBasis_closed.uniformity_compacts.comap _ |>.ge_iff]
+  intro U ⟨hU₁, hU₂⟩
+  filter_upwards [hf hU₁] with K hK
+  simp_rw [Set.mem_preimage, Prod.map, id, mem_hausdorffEntourage]
+  constructor
+  · intro x hx
+    let lx := l ⊓ 𝓟 (UniformSpace.ball x U)
+    have hlx : lx.TotallyBounded := hl.mono inf_le_left
+    have : lx.NeBot := by
+      unfold lx l
+      rw [Filter.lift'_inf_principal_eq, Filter.lift'_neBot_iff fun _ _ h =>
+        Set.inter_subset_inter_left _ <| Set.biUnion_subset_biUnion_left h]
+      intro s hs
+      obtain ⟨K', ⟨h₁, -⟩, h₂⟩ := Filter.nonempty_of_mem <| Filter.inter_mem hK hs
+      obtain ⟨y, hy, hxy⟩ := h₁ hx
+      exact ⟨y, Set.mem_iUnion₂_of_mem h₂ hy, hxy⟩
+    obtain ⟨y, hy⟩ := hlx.exists_clusterPt
+    have hy₁ : ClusterPt y l := .of_inf_left hy
+    have hy₂ : ClusterPt y (𝓟 (UniformSpace.ball x U)) := .of_inf_right hy
+    rw [← mem_closure_iff_clusterPt, (UniformSpace.isClosed_ball x hU₂).closure_eq] at hy₂
+    exact ⟨y, hy₁, hy₂⟩
+  · intro x (hx : ClusterPt x l)
+    rw [← (hU₂.relImage_of_isCompact K.isCompact).closure_eq, mem_closure_iff_clusterPt]
+    refine hx.mono ?_
+    rw [Filter.le_principal_iff]
+    refine Filter.mem_of_superset (Filter.mem_lift' hK) ?_
+    rw [Set.iUnion₂_subset_iff]
+    exact fun _ ⟨_, h⟩ => h
+
 end TopologicalSpace.Compacts
 
 namespace TopologicalSpace.NonemptyCompacts
@@ -486,6 +535,16 @@ theorem isEmbedding_toCompacts : IsEmbedding (toCompacts (α := α)) :=
 theorem continuous_toCompacts : Continuous (toCompacts (α := α)) :=
   uniformContinuous_toCompacts.continuous
 
+@[fun_prop]
+theorem isClosedEmbedding_toCompacts : IsClosedEmbedding (toCompacts (α := α)) where
+  __ := isEmbedding_toCompacts
+  isClosed_range := by
+    rw [range_toCompacts, isClosed_compl_iff]
+    convert (UniformSpace.hausdorff.isClopen_singleton_empty (α := α))
+      |>.isOpen.preimage Compacts.uniformContinuous_coe.continuous
+    rw [← Compacts.coe_bot, ← Set.image_singleton (f := SetLike.coe),
+      SetLike.coe_injective.preimage_image]
+
 theorem isOpen_inter_nonempty_of_isOpen {s : Set α} (hs : IsOpen s) :
     IsOpen {t : NonemptyCompacts α | ((t : Set α) ∩ s).Nonempty} :=
   isOpen_induced (UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen hs)
@@ -529,4 +588,27 @@ theorem _root_.IsUniformEmbedding.nonemptyCompacts_map {f : α → β} (hf : IsU
   __ := hf.isUniformInducing.nonemptyCompacts_map
   injective := map_injective hf.uniformContinuous.continuous hf.injective
 
+instance [CompleteSpace α] : CompleteSpace (NonemptyCompacts α) :=
+  isUniformEmbedding_toCompacts.completeSpace isClosedEmbedding_toCompacts.isClosed_range.isComplete
+
+@[simp]
+theorem completeSpace_iff : CompleteSpace (NonemptyCompacts α) ↔ CompleteSpace α := by
+  refine ⟨fun _ => ⟨fun {f} hf => ?_⟩, fun _ => inferInstance⟩
+  obtain ⟨K, hK⟩ := CompleteSpace.complete <| hf.map uniformContinuous_singleton
+  obtain ⟨x, hx⟩ := K.nonempty
+  exists x
+  rw [(nhds_basis_opens x).ge_iff]
+  intro U ⟨hxU, hU⟩
+  filter_upwards [hK <| (isOpen_inter_nonempty_of_isOpen hU).mem_nhds ⟨x, hx, hxU⟩]
+  simp
+
+@[simp]
+theorem _root_.TopologicalSpace.Compacts.completeSpace_iff :
+    CompleteSpace (Compacts α) ↔ CompleteSpace α where
+  mp _ :=
+    NonemptyCompacts.completeSpace_iff.mp <|
+      NonemptyCompacts.isUniformEmbedding_toCompacts.completeSpace
+        isClosedEmbedding_toCompacts.isClosed_range.isComplete
+  mpr _ := inferInstance
+
 end TopologicalSpace.NonemptyCompacts