feat(Topology/Sets): define the Vietoris topology on (Nonempty)Compacts

This PR defines the Vietoris topology on `Compacts` and `NonemptyCompacts`, and proves that it is induced by the Hausdorff uniformity.

Author: gasparattila

Mathlib/Data/Rel.lean

@@ -459,6 +459,9 @@ lemma prod_subset_comm [R.IsSymm] : s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆
   rw [← R.inv_eq_self, SetRel.inv, ← Set.image_subset_iff, Set.image_swap_prod, ← SetRel.inv,
     R.inv_eq_self]
 
+lemma preimage_eq_image [R.IsSymm] : R.preimage s = R.image s := by
+  rw [← preimage_inv, inv_eq_self]
+
 variable (R) in
 /-- The maximal symmetric relation contained in a given relation. -/
 def symmetrize : SetRel α α := R ∩ R.inv

Mathlib/Topology/MetricSpace/Closeds.lean

@@ -269,7 +269,9 @@ namespace NonemptyCompacts
 /-- In an emetric space, the type of non-empty compact subsets is an emetric space,
 where the edistance is the Hausdorff edistance -/
 instance emetricSpace : EMetricSpace (NonemptyCompacts α) where
-  __ := PseudoEMetricSpace.hausdorff.induced SetLike.coe
+  /- Since the topology on `NonemptyCompacts` is not defeq to the one induced by the metric, we
+  replace the uniformity by `NonemptyCompacts.uniformSpace`, which has the right topology. -/
+  __ := (PseudoEMetricSpace.hausdorff.induced SetLike.coe).replaceUniformity <| by rfl
   eq_of_edist_eq_zero {s t} h := NonemptyCompacts.ext <| by
     have : closure (s : Set α) = closure t := hausdorffEdist_zero_iff_closure_eq_closure.1 h
     rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this

Mathlib/Topology/Sets/Compacts.lean

@@ -22,7 +22,7 @@ For a topological space `α`,
 -/
 
 
-open Set
+open Set Topology
 
 variable {α β γ : Type*} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ]
 
@@ -209,6 +209,34 @@ theorem singleton_prod_singleton (x : α) (y : β) :
     Compacts.prod {x} {y} = {(x, y)} :=
   Compacts.ext Set.singleton_prod_singleton
 
+/-- The Vietoris topology on the compact subsets of a topological space. -/
+instance topology : TopologicalSpace (Compacts α) :=
+  .generateFrom <|
+    (fun U => {K | (K : Set α) ⊆ U}) '' {U | IsOpen U} ∪
+    (fun V => {K | ((K : Set α) ∩ V).Nonempty}) '' {V | IsOpen V}
+
+theorem isOpen_subsets_of_isOpen {U : Set α} (h : IsOpen U) :
+    IsOpen {K : Compacts α | (K : Set α) ⊆ U} :=
+  isOpen_generateFrom_of_mem <| .inl ⟨U, h, rfl⟩
+
+theorem isOpen_inter_nonempty_of_isOpen {U : Set α} (h : IsOpen U) :
+    IsOpen {K : Compacts α | ((K : Set α) ∩ U).Nonempty} :=
+  isOpen_generateFrom_of_mem <| .inr ⟨U, h, rfl⟩
+
+theorem isClosed_subsets_of_isClosed {F : Set α} (h : IsClosed F) :
+    IsClosed {K : Compacts α | (K : Set α) ⊆ F} := by
+  simp_rw [← isOpen_compl_iff, Set.compl_setOf, ← Set.inter_compl_nonempty_iff]
+  exact isOpen_inter_nonempty_of_isOpen h.isOpen_compl
+
+theorem isClosed_inter_nonempty_of_isClosed {F : Set α} (h : IsClosed F) :
+    IsClosed {K : Compacts α | ((K : Set α) ∩ F).Nonempty} := by
+  simp_rw +singlePass [← compl_compl F, Set.inter_compl_nonempty_iff, ← Set.compl_setOf]
+  exact (isOpen_subsets_of_isOpen h.isOpen_compl).isClosed_compl
+
+theorem isClopen_singleton_bot : IsClopen {(⊥ : Compacts α)} := by
+  simp_rw [← Set.setOf_eq_eq_singleton, ← SetLike.coe_set_eq, coe_bot, ← subset_empty_iff]
+  exact ⟨isClosed_subsets_of_isClosed isClosed_empty, isOpen_subsets_of_isOpen isOpen_empty⟩
+
 -- todo: add `pi`
 
 end Compacts
@@ -242,6 +270,14 @@ protected theorem nonempty (s : NonemptyCompacts α) : (s : Set α).Nonempty :=
 theorem toCompacts_injective : Function.Injective (toCompacts (α := α)) :=
   .of_comp (f := SetLike.coe) SetLike.coe_injective
 
+theorem range_toCompacts : Set.range (toCompacts (α := α)) = {⊥}ᶜ := by
+  ext K
+  simp_rw [Set.mem_compl_singleton_iff, ← SetLike.coe_set_eq.ne, Compacts.coe_bot,
+    ← Set.nonempty_iff_ne_empty]
+  refine ⟨?_, fun h => ⟨⟨K, h⟩, rfl⟩⟩
+  rintro ⟨K, _, rfl⟩
+  exact K.nonempty
+
 /-- Reinterpret a nonempty compact as a closed set. -/
 def toCloseds [T2Space α] (s : NonemptyCompacts α) : Closeds α :=
   ⟨s, s.isCompact.isClosed⟩
@@ -332,6 +368,53 @@ theorem singleton_prod_singleton (x : α) (y : β) :
     NonemptyCompacts.prod {x} {y} = {(x, y)} :=
   NonemptyCompacts.ext Set.singleton_prod_singleton
 
+/-- The Vietoris topology on the nonempty compact subsets of a topological space. -/
+instance topology : TopologicalSpace (NonemptyCompacts α) :=
+  TopologicalSpace.generateFrom
+    ((fun U => {K : NonemptyCompacts α | (K : Set α) ⊆ U}) '' {U | IsOpen U} ∪
+    (fun V => {K : NonemptyCompacts α | ((K : Set α) ∩ V).Nonempty}) '' {V | IsOpen V})
+
+@[fun_prop]
+theorem isEmbedding_toCompacts : IsEmbedding (toCompacts (α := α)) where
+  injective := toCompacts_injective
+  eq_induced := by
+    simp_rw [topology, Compacts.topology, induced_generateFrom_eq, image_union, image_image,
+      preimage_setOf_eq, coe_toCompacts]
+
+@[fun_prop]
+theorem continuous_toCompacts : Continuous (toCompacts (α := α)) :=
+  isEmbedding_toCompacts.continuous
+
+@[fun_prop]
+theorem isClosedEmbedding_toCompacts : IsClosedEmbedding (toCompacts (α := α)) where
+  __ := isEmbedding_toCompacts
+  isClosed_range := by
+    rw [range_toCompacts]
+    exact Compacts.isClopen_singleton_bot.compl.isClosed
+
+@[fun_prop]
+theorem isOpenEmbedding_toCompacts : IsOpenEmbedding (toCompacts (α := α)) where
+  __ := isEmbedding_toCompacts
+  isOpen_range := by
+    rw [range_toCompacts]
+    exact Compacts.isClopen_singleton_bot.compl.isOpen
+
+theorem isOpen_subsets_of_isOpen {U : Set α} (h : IsOpen U) :
+    IsOpen {K : NonemptyCompacts α | (K : Set α) ⊆ U} :=
+  (Compacts.isOpen_subsets_of_isOpen h).preimage continuous_toCompacts
+
+theorem isOpen_inter_nonempty_of_isOpen {U : Set α} (h : IsOpen U) :
+    IsOpen {K : NonemptyCompacts α | ((K : Set α) ∩ U).Nonempty} :=
+  (Compacts.isOpen_inter_nonempty_of_isOpen h).preimage continuous_toCompacts
+
+theorem isClosed_subsets_of_isClosed {F : Set α} (h : IsClosed F) :
+    IsClosed {K : NonemptyCompacts α | (K : Set α) ⊆ F} :=
+  (Compacts.isClosed_subsets_of_isClosed h).preimage continuous_toCompacts
+
+theorem isClosed_inter_nonempty_of_isClosed {F : Set α} (h : IsClosed F) :
+    IsClosed {K : NonemptyCompacts α | ((K : Set α) ∩ F).Nonempty} :=
+  (Compacts.isClosed_inter_nonempty_of_isClosed h).preimage continuous_toCompacts
+
 end NonemptyCompacts
 
 /-! ### Positive compact sets -/

Mathlib/Topology/UniformSpace/Closeds.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Attila Gáspár
 -/
 import Mathlib.Topology.Sets.Compacts
+import Mathlib.Topology.UniformSpace.Compact
 import Mathlib.Topology.UniformSpace.UniformEmbedding
 
 /-!
@@ -74,6 +75,18 @@ instance isTrans_hausdorffEntourage (U : SetRel α α) [hU : U.IsTrans] :
     (hausdorffEntourage U).IsTrans := by
   grw [isTrans_iff_comp_subset_self, ← hausdorffEntourage_comp, comp_subset_self]
 
+theorem TotallyBounded.exists_prodMk_finset_mem_hausdorffEntourage [UniformSpace α]
+    {s : Set α} (hs : TotallyBounded s) {U : SetRel α α} (hU : U ∈ 𝓤 α) :
+    ∃ t : Finset α, (↑t, s) ∈ hausdorffEntourage U := by
+  obtain ⟨t, ht₁, ht₂⟩ := hs _ (symm_le_uniformity hU)
+  lift t to Finset α using ht₁
+  classical
+  refine ⟨{x ∈ t | ∃ y ∈ s, (x, y) ∈ U}, ?_⟩
+  rw [Finset.coe_filter]
+  refine ⟨fun _ h => h.2, fun x hx => ?_⟩
+  obtain ⟨y, hy, hxy⟩ := Set.mem_iUnion₂.mp (ht₂ hx)
+  exact ⟨y, ⟨hy, x, hx, hxy⟩, hxy⟩
+
 end hausdorffEntourage
 
 variable [UniformSpace α]
@@ -154,8 +167,41 @@ end TopologicalSpace.Closeds
 
 namespace TopologicalSpace.Compacts
 
+open UniformSpace in
 instance uniformSpace : UniformSpace (Compacts α) :=
-  .comap SetLike.coe .hausdorff
+  .replaceTopology (.comap SetLike.coe .hausdorff) <| by
+    -- We need to show that the Hausdorff uniformity induces the Vietoris topology
+    refine le_antisymm (le_of_nhds_le_nhds fun K => ?_) ?_
+    · simp_rw [nhds_eq_comap_uniformity]
+      change _ ≤ Filter.comap _ (Filter.comap _ (Filter.lift' _ _))
+      rw [Filter.comap_comap,
+        uniformity_hasBasis_open.lift' monotone_hausdorffEntourage |>.comap _ |>.ge_iff]
+      intro U ⟨hU₁, hU₂⟩
+      simp_rw [Function.comp_id, hausdorffEntourage, Set.preimage_setOf_eq, Function.comp,
+        Set.setOf_and]
+      have : U.IsRefl := ⟨fun _ => refl_mem_uniformity hU₁⟩
+      refine Filter.inter_mem ?_ <| (isOpen_subsets_of_isOpen hU₂.relImage).mem_nhds <|
+        SetRel.self_subset_image _
+      obtain ⟨V : SetRel α α, hV₁, hV₂, _, hVU⟩ := comp_open_symm_mem_uniformity_sets hU₁
+      obtain ⟨s, hs₁, hs₂⟩ :=
+        K.isCompact.totallyBounded.exists_prodMk_finset_mem_hausdorffEntourage hV₁
+      dsimp only at hs₁ hs₂
+      filter_upwards [(Filter.eventually_all_finset s).mpr fun x hx =>
+        isOpen_inter_nonempty_of_isOpen (isOpen_ball x hV₂) |>.eventually_mem (hs₁ hx)] with L hL
+      grw [hs₂, ← SetRel.preimage_eq_image, ← hVU, SetRel.preimage_comp]
+      gcongr
+      exact hL
+    · apply le_generateFrom
+      rintro _ (⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩)
+      · simp_rw [isOpen_iff_mem_nhds, UniformSpace.mem_nhds_iff]
+        intro K hK
+        obtain ⟨V, hV₁, hV₂⟩ :=
+          K.isCompact.nhdsSet_basis_uniformity (𝓤 _).basis_sets
+            |>.mem_iff.mp (hU.mem_nhdsSet.mpr hK)
+        rw [Set.iUnion₂_subset_iff] at hV₂
+        exact ⟨_, Filter.preimage_mem_comap (Filter.mem_lift' hV₁),
+          fun L ⟨_, hL⟩ x hx => (hL hx).elim fun y ⟨hy, hyx⟩ => hV₂ y hy hyx⟩
+      · exact isOpen_induced (hausdorff.isOpen_inter_nonempty_of_isOpen hU)
 
 theorem uniformity_def :
     𝓤 (Compacts α) = .comap (Prod.map (↑) (↑)) ((𝓤 α).lift' hausdorffEntourage) :=
@@ -173,20 +219,17 @@ theorem isUniformEmbedding_coe : IsUniformEmbedding ((↑) : Compacts α → Set
 theorem uniformContinuous_coe : UniformContinuous ((↑) : Compacts α → Set α) :=
   isUniformEmbedding_coe.uniformContinuous
 
-theorem isOpen_inter_nonempty_of_isOpen {s : Set α} (hs : IsOpen s) :
-    IsOpen {t : Compacts α | ((t : Set α) ∩ s).Nonempty} :=
-  isOpen_induced (UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen hs)
-
-theorem isClosed_subsets_of_isClosed {s : Set α} (hs : IsClosed s) :
-    IsClosed {t : Compacts α | (t : Set α) ⊆ s} :=
-  isClosed_induced (UniformSpace.hausdorff.isClosed_subsets_of_isClosed hs)
-
 end TopologicalSpace.Compacts
 
 namespace TopologicalSpace.NonemptyCompacts
 
 instance uniformSpace : UniformSpace (NonemptyCompacts α) :=
-  .comap SetLike.coe .hausdorff
+  .replaceTopology (.comap SetLike.coe .hausdorff) <| by
+    rw [isEmbedding_toCompacts.eq_induced]
+    change (Compacts.uniformSpace.comap toCompacts).toTopologicalSpace = _
+    congr 1
+    ext1
+    exact Filter.comap_comap
 
 theorem uniformity_def :
     𝓤 (NonemptyCompacts α) = .comap (Prod.map (↑) (↑)) ((𝓤 α).lift' hausdorffEntourage) :=
@@ -227,16 +270,4 @@ theorem isUniformEmbedding_toCompacts : IsUniformEmbedding (toCompacts (α := α
 theorem uniformContinuous_toCompacts : UniformContinuous (toCompacts (α := α)) :=
   isUniformEmbedding_toCompacts.uniformContinuous
 
-@[fun_prop]
-theorem continuous_toCompacts : Continuous (toCompacts (α := α)) :=
-  uniformContinuous_toCompacts.continuous
-
-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)
-
-theorem isClosed_subsets_of_isClosed {s : Set α} (hs : IsClosed s) :
-    IsClosed {t : NonemptyCompacts α | (t : Set α) ⊆ s} :=
-  isClosed_induced (UniformSpace.hausdorff.isClosed_subsets_of_isClosed hs)
-
 end TopologicalSpace.NonemptyCompacts