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

Mathlib.lean

@@ -7366,6 +7366,7 @@ public import Mathlib.Topology.Sets.Compacts
 public import Mathlib.Topology.Sets.OpenCover
 public import Mathlib.Topology.Sets.Opens
 public import Mathlib.Topology.Sets.Order
+public import Mathlib.Topology.Sets.VietorisTopology
 public import Mathlib.Topology.Sheaves.Alexandrov
 public import Mathlib.Topology.Sheaves.CommRingCat
 public import Mathlib.Topology.Sheaves.Forget

Mathlib/Data/Rel.lean

@@ -490,6 +490,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

@@ -226,7 +226,10 @@ 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 instEMetricSpace : EMetricSpace (NonemptyCompacts α) where
-  __ := PseudoEMetricSpace.hausdorff.induced SetLike.coe
+  /- Since the topology on `NonemptyCompacts` is not defeq to the one induced by
+  `UniformSpace.hausdorff`, 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

@@ -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/Sets/VietorisTopology.lean

@@ -0,0 +1,176 @@
+/-
+Copyright (c) 2025 Attila Gáspár. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Attila Gáspár
+-/
+module
+
+public import Mathlib.Topology.Sets.Compacts
+
+/-!
+# Vietoris topology
+
+This file defines the Vietoris topology on the types of compact subsets and nonempty compact subsets
+of a topological space. The Vietoris topology is generated by sets of the form
+$\{K \mid K \subseteq U\}$ and $\{K \mid K \cap U \ne \emptyset\}$, where $U$ is an open subset of
+the underlying space.
+
+## Implementation notes
+
+Rather than defining the topology directly on `TopologicalSpace.Compacts α`, we first define
+`TopologicalSpace.vietoris α` on `Set α`, then we take the subspace topology on
+`TopologicalSpace.Compacts α` and `TopologicalSpace.NonemptyCompacts α`. This approach will
+let us reuse several results if a type of closed sets equipped with the Vietoris topology is
+defined in the future.
+
+Note that we do not equip `TopologicalSpace.Closeds α` with the Vietoris topology. When `α` is a
+metric space, `TopologicalSpace.Closeds α` is equipped with the Hausdorff metric, which is generally
+incompatible with the Vietoris topology.
+
+## References
+
+* [Ernest Michael, *Topologies on spaces of subsets*][michael1951]
+-/
+
+@[expose] public section
+
+open Set Topology
+
+variable (α : Type*) [TopologicalSpace α]
+
+namespace TopologicalSpace
+
+/-- The Vietoris topology on the powerset of a topological space, generated by sets of the form
+`{A | A ⊆ U}` and `{A | A ∩ U ≠ ∅}`, where `U` is an open subset of the underlying space. Used for
+defining the topologies on `Compacts` and `NonemptyCompacts`. -/
+protected def vietoris : TopologicalSpace (Set α) :=
+  .generateFrom <| powerset '' {U | IsOpen U} ∪ (fun V => {s | (s ∩ V).Nonempty}) '' {V | IsOpen V}
+
+attribute [local instance] TopologicalSpace.vietoris
+
+variable {α}
+
+namespace vietoris
+
+/-- When `Set` is equipped with the Vietoris topology, the powerset of an open set is open. -/
+theorem _root_.IsOpen.powerset_vietoris {U : Set α} (h : IsOpen U) :
+    IsOpen U.powerset :=
+  isOpen_generateFrom_of_mem <| .inl ⟨U, h, rfl⟩
+
+theorem isOpen_inter_nonempty_of_isOpen {U : Set α} (h : IsOpen U) :
+    IsOpen {s | (s ∩ U).Nonempty} :=
+  isOpen_generateFrom_of_mem <| .inr ⟨U, h, rfl⟩
+
+/-- When `Set` is equipped with the Vietoris topology, the powerset of a closed set is closed. -/
+theorem _root_.IsClosed.powerset_vietoris {F : Set α} (h : IsClosed F) :
+    IsClosed F.powerset := by
+  simp_rw [powerset, ← isOpen_compl_iff, compl_setOf, ← 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 {s | (s ∩ F).Nonempty} := by
+  simp_rw +singlePass [← compl_compl F, inter_compl_nonempty_iff, ← compl_setOf]
+  exact h.isOpen_compl.powerset_vietoris.isClosed_compl
+
+theorem isClopen_singleton_empty : IsClopen {(∅ : Set α)} := by
+  rw [← powerset_empty]
+  exact ⟨isClosed_empty.powerset_vietoris, isOpen_empty.powerset_vietoris⟩
+
+end vietoris
+
+namespace Compacts
+
+/-- The Vietoris topology on the compact subsets of a topological space. -/
+instance topology : TopologicalSpace (Compacts α) :=
+  .induced (↑) (.vietoris α)
+
+@[fun_prop]
+theorem isEmbedding_coe : IsEmbedding ((↑) : Compacts α → Set α) where
+  injective := SetLike.coe_injective
+  eq_induced := rfl
+
+@[fun_prop]
+theorem continuous_coe : Continuous ((↑) : Compacts α → Set α) :=
+  isEmbedding_coe.continuous
+
+theorem isOpen_subsets_of_isOpen {U : Set α} (h : IsOpen U) :
+    IsOpen {K : Compacts α | ↑K ⊆ U} :=
+  continuous_coe.isOpen_preimage _ h.powerset_vietoris
+
+theorem isOpen_inter_nonempty_of_isOpen {U : Set α} (h : IsOpen U) :
+    IsOpen {K : Compacts α | (↑K ∩ U).Nonempty} :=
+  continuous_coe.isOpen_preimage _ <| vietoris.isOpen_inter_nonempty_of_isOpen h
+
+theorem isClosed_subsets_of_isClosed {F : Set α} (h : IsClosed F) :
+    IsClosed {K : Compacts α | ↑K ⊆ 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 ∩ 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
+  convert vietoris.isClopen_singleton_empty.preimage continuous_coe
+  rw [← coe_bot, ← image_singleton (f := SetLike.coe), SetLike.coe_injective.preimage_image]
+
+end Compacts
+
+namespace NonemptyCompacts
+
+/-- The Vietoris topology on the nonempty compact subsets of a topological space. -/
+instance topology : TopologicalSpace (NonemptyCompacts α) :=
+  .induced (↑) (.vietoris α)
+
+@[fun_prop]
+theorem isEmbedding_coe : IsEmbedding ((↑) : NonemptyCompacts α → Set α) where
+  injective := SetLike.coe_injective
+  eq_induced := rfl
+
+@[fun_prop]
+theorem continuous_coe : Continuous ((↑) : NonemptyCompacts α → Set α) :=
+  isEmbedding_coe.continuous
+
+@[fun_prop]
+theorem isEmbedding_toCompacts : IsEmbedding (toCompacts (α := α)) where
+  injective := toCompacts_injective
+  eq_induced := .symm <| induced_compose (f := toCompacts) (g := SetLike.coe)
+
+@[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 ⊆ U} :=
+  h.powerset_vietoris.preimage continuous_coe
+
+theorem isOpen_inter_nonempty_of_isOpen {U : Set α} (h : IsOpen U) :
+    IsOpen {K : NonemptyCompacts α | (↑K ∩ U).Nonempty} :=
+  (vietoris.isOpen_inter_nonempty_of_isOpen h).preimage continuous_coe
+
+theorem isClosed_subsets_of_isClosed {F : Set α} (h : IsClosed F) :
+    IsClosed {K : NonemptyCompacts α | ↑K ⊆ F} :=
+  h.powerset_vietoris.preimage continuous_coe
+
+theorem isClosed_inter_nonempty_of_isClosed {F : Set α} (h : IsClosed F) :
+    IsClosed {K : NonemptyCompacts α | (↑K ∩ F).Nonempty} :=
+  (vietoris.isClosed_inter_nonempty_of_isClosed h).preimage continuous_coe
+
+end NonemptyCompacts
+
+end TopologicalSpace

Mathlib/Topology/UniformSpace/Closeds.lean

@@ -6,9 +6,11 @@ Authors: Attila Gáspár
 module
 
 public import Mathlib.Topology.Order.Lattice
-public import Mathlib.Topology.Sets.Compacts
+public import Mathlib.Topology.Sets.VietorisTopology
 public import Mathlib.Topology.UniformSpace.UniformEmbedding
 
+import Mathlib.Topology.UniformSpace.Compact
+
 /-!
 # Hausdorff uniformity
 
@@ -89,6 +91,18 @@ theorem union_mem_hausdorffEntourage (U : SetRel α α) {s₁ s₂ t₁ t₂ : S
     (s₁ ∪ s₂, t₁ ∪ t₂) ∈ hausdorffEntourage U := by
   grind [mem_hausdorffEntourage, preimage_union, image_union]
 
+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 α] [UniformSpace β]
@@ -255,6 +269,41 @@ theorem TotallyBounded.powerset_hausdorff {t : Set α} (ht : TotallyBounded t) :
   obtain ⟨y, hy, hxy⟩ := Set.mem_iUnion₂.mp (ht (hs hx))
   exact ⟨y, ⟨hy, ⟨x, hx, hxy⟩⟩, hxy⟩
 
+/-- The neighborhoods of a totally bounded set in the Hausdorff uniformity are neighborhoods in the
+Vietoris topology. -/
+theorem TotallyBounded.nhds_vietoris_le_nhds_hausdorff {s : Set α} (hs : TotallyBounded s) :
+    @nhds _ (.vietoris α) s ≤ 𝓝 s := by
+  open UniformSpace TopologicalSpace.vietoris in
+  simp_rw [nhds_eq_comap_uniformity,
+    uniformity_hasBasis_open.uniformity_hausdorff |>.comap _ |>.ge_iff, Function.comp_id,
+    hausdorffEntourage, Set.preimage_setOf_eq, Set.setOf_and]
+  intro U ⟨hU₁, hU₂⟩
+  have : U.IsRefl := ⟨fun _ => refl_mem_uniformity hU₁⟩
+  let := TopologicalSpace.vietoris α
+  refine Filter.inter_mem ?_ <| hU₂.relImage.powerset_vietoris.mem_nhds <|
+    SetRel.self_subset_image _
+  obtain ⟨V : SetRel α α, hV₁, hV₂, _, hVU⟩ := comp_open_symm_mem_uniformity_sets hU₁
+  obtain ⟨t, ht₁, ht₂⟩ := hs.exists_prodMk_finset_mem_hausdorffEntourage hV₁
+  dsimp only at ht₁ ht₂
+  filter_upwards [(Filter.eventually_all_finset t).mpr fun x hx =>
+    isOpen_inter_nonempty_of_isOpen (isOpen_ball x hV₂) |>.eventually_mem (ht₁ hx)]
+    with u (hu : ↑t ⊆ V.preimage ↑u)
+  grw [ht₂, ← SetRel.preimage_eq_image, hu, ← hVU, SetRel.preimage_comp]
+
+/-- A compact set has the same neighborhoods in the Hausdorff uniformity and the Vietoris topology.
+-/
+theorem IsCompact.nhds_hausdorff_eq_nhds_vietoris {s : Set α} (hs : IsCompact s) :
+    𝓝 s = @nhds _ (.vietoris α) s := by
+  refine le_antisymm ?_ hs.totallyBounded.nhds_vietoris_le_nhds_hausdorff
+  simp_rw [TopologicalSpace.nhds_generateFrom, le_iInf₂_iff, Filter.le_principal_iff]
+  rintro _ ⟨hs', (⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩)⟩
+  · obtain ⟨V : SetRel α α, hV₁, hV₂⟩ :=
+      hs.nhdsSet_basis_uniformity (𝓤 α).basis_sets |>.mem_iff.mp (hU.mem_nhdsSet.mpr hs')
+    filter_upwards [UniformSpace.ball_mem_nhds _ (Filter.mem_lift' hV₁)]
+      with t ⟨_, ht⟩
+    exact ht.trans fun x ⟨y, hy, hxy⟩ => hV₂ <| Set.mem_biUnion hy hxy
+  · exact (UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen hU).mem_nhds hs'
+
 namespace TopologicalSpace.Closeds
 
 instance uniformSpace : UniformSpace (Closeds α) :=
@@ -356,7 +405,8 @@ end TopologicalSpace.Closeds
 namespace TopologicalSpace.Compacts
 
 instance uniformSpace : UniformSpace (Compacts α) :=
-  .comap (↑) (.hausdorff α)
+  .replaceTopology (.comap (↑) (.hausdorff α)) <| ext_nhds fun K =>  by
+    simp_rw [nhds_induced, K.isCompact.nhds_hausdorff_eq_nhds_vietoris]
 
 theorem uniformity_def :
     𝓤 (Compacts α) = .comap (Prod.map (↑) (↑)) ((𝓤 α).lift' hausdorffEntourage) :=
@@ -389,14 +439,6 @@ theorem isEmbedding_toCloseds [T2Space α] : IsEmbedding (toCloseds (α := α))
 theorem continuous_toCloseds [T2Space α] : Continuous (toCloseds (α := α)) :=
   uniformContinuous_toCloseds.continuous
 
-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 hs.powerset_hausdorff
-
 theorem totallyBounded_subsets_of_totallyBounded {t : Set α} (ht : TotallyBounded t) :
     TotallyBounded {K : Compacts α | ↑K ⊆ t} :=
   totallyBounded_preimage isUniformEmbedding_coe.isUniformInducing ht.powerset_hausdorff
@@ -437,7 +479,8 @@ end TopologicalSpace.Compacts
 namespace TopologicalSpace.NonemptyCompacts
 
 instance uniformSpace : UniformSpace (NonemptyCompacts α) :=
-  .comap (↑) (.hausdorff α)
+  .replaceTopology (.comap (↑) (.hausdorff α)) <| ext_nhds fun K =>  by
+    simp_rw [nhds_induced, K.isCompact.nhds_hausdorff_eq_nhds_vietoris]
 
 theorem uniformity_def :
     𝓤 (NonemptyCompacts α) = .comap (Prod.map (↑) (↑)) ((𝓤 α).lift' hausdorffEntourage) :=
@@ -478,22 +521,6 @@ theorem isUniformEmbedding_toCompacts : IsUniformEmbedding (toCompacts (α := α
 theorem uniformContinuous_toCompacts : UniformContinuous (toCompacts (α := α)) :=
   isUniformEmbedding_toCompacts.uniformContinuous
 
-@[fun_prop]
-theorem isEmbedding_toCompacts : IsEmbedding (toCompacts (α := α)) :=
-  isUniformEmbedding_toCompacts.isEmbedding
-
-@[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 hs.powerset_hausdorff
-
 theorem totallyBounded_subsets_of_totallyBounded {t : Set α} (ht : TotallyBounded t) :
     TotallyBounded {K : NonemptyCompacts α | ↑K ⊆ t} :=
   totallyBounded_preimage isUniformEmbedding_coe.isUniformInducing ht.powerset_hausdorff

docs/references.bib

@@ -3659,6 +3659,17 @@ @Book{            meyntweedie1993
   language      = {English}
 }
 
+@Article{         michael1951,
+  author        = {Michael, Ernest},
+  title         = {Topologies on spaces of subsets},
+  year          = {1951},
+  journal       = {Trans. Amer. Math. Soc.},
+  volume        = {71},
+  pages         = {152-182},
+  doi           = {10.1090/S0002-9947-1951-0042109-4},
+  url           = {https://doi.org/10.1090/S0002-9947-1951-0042109-4}
+}
+
 @Article{         Milla_2018,
   author        = {Milla, Lorenz},
   title         = {A detailed proof of the {C}hudnovsky formula with means of