feat(Topology/UniformSpace): define the Hausdorff uniformity (#31031)

This PR defines the Hausdorff uniformity on `Closeds`, `Compacts` and `NonemptyCompacts`. Since `Closeds` and `NonemptyCompacts` already have metrics, they are changed to use the newly defined uniformity.

Co-authored-by: Oliver Nash <github@olivernash.org>

Author: gasparattila

Mathlib.lean

@@ -7150,6 +7150,7 @@ public import Mathlib.Topology.UniformSpace.AbstractCompletion
 public import Mathlib.Topology.UniformSpace.Ascoli
 public import Mathlib.Topology.UniformSpace.Basic
 public import Mathlib.Topology.UniformSpace.Cauchy
+public import Mathlib.Topology.UniformSpace.Closeds
 public import Mathlib.Topology.UniformSpace.Compact
 public import Mathlib.Topology.UniformSpace.CompactConvergence
 public import Mathlib.Topology.UniformSpace.CompareReals

Mathlib/Data/Rel.lean

@@ -223,9 +223,15 @@ def preimage : Set α := {a | ∃ b ∈ t, a ~[R] b}
 @[gcongr] lemma image_subset_image (hs : s₁ ⊆ s₂) : image R s₁ ⊆ image R s₂ :=
   fun _ ⟨a, ha, hab⟩ ↦ ⟨a, hs ha, hab⟩
 
+@[gcongr] lemma image_subset_image_left (hR : R₁ ⊆ R₂) : image R₁ s ⊆ image R₂ s :=
+  fun _ ⟨a, ha, hab⟩ ↦ ⟨a, ha, hR hab⟩
+
 @[gcongr] lemma preimage_subset_preimage (ht : t₁ ⊆ t₂) : preimage R t₁ ⊆ preimage R t₂ :=
   fun _ ⟨a, ha, hab⟩ ↦ ⟨a, ht ha, hab⟩
 
+@[gcongr] lemma preimage_subset_preimage_left (hR : R₁ ⊆ R₂) : preimage R₁ t ⊆ preimage R₂ t :=
+  fun _ ⟨a, ha, hab⟩ ↦ ⟨a, ha, hR hab⟩
+
 variable (R t) in
 @[simp] lemma image_inv : R.inv.image t = preimage R t := rfl
 
@@ -385,6 +391,12 @@ lemma subset_iterate_comp [R.IsRefl] {S : SetRel α β} : ∀ {n}, S ⊆ (R ○
   | 0 => .rfl
   | _n + 1 => right_subset_comp.trans subset_iterate_comp
 
+lemma self_subset_image [R.IsRefl] (s : Set α) : s ⊆ R.image s :=
+  fun x hx => ⟨x, hx, R.rfl⟩
+
+lemma self_subset_preimage [R.IsRefl] (s : Set α) : s ⊆ R.preimage s :=
+  fun x hx => ⟨x, hx, R.rfl⟩
+
 lemma exists_eq_singleton_of_prod_subset_id {s t : Set α} (hs : s.Nonempty) (ht : t.Nonempty)
     (hst : s ×ˢ t ⊆ SetRel.id) : ∃ x, s = {x} ∧ t = {x} := by
   obtain ⟨a, ha⟩ := hs

Mathlib/Topology/MetricSpace/Closeds.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Analysis.SpecificLimits.Basic
 public import Mathlib.Topology.MetricSpace.HausdorffDistance
-public import Mathlib.Topology.Sets.Compacts
+public import Mathlib.Topology.UniformSpace.Closeds
 
 /-!
 # Closed subsets
@@ -34,15 +34,60 @@ namespace EMetric
 
 section
 
+variable {α : Type*} [PseudoEMetricSpace α]
+
+theorem mem_hausdorffEntourage_of_hausdorffEdist_lt {s t : Set α} {δ : ℝ≥0∞}
+    (h : hausdorffEdist s t < δ) : (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 < δ} := by
+  rw [hausdorffEdist, max_lt_iff] at h
+  rw [hausdorffEntourage, Set.mem_setOf]
+  conv => enter [2, 2, 1, 1, _]; rw [edist_comm]
+  have {s t : Set α} (h : ⨆ x ∈ s, infEdist x t < δ) :
+      s ⊆ SetRel.preimage {p | edist p.1 p.2 < δ} t := by
+    intro x hx
+    simpa only [infEdist, iInf_lt_iff, exists_prop] using (le_iSup₂ x hx).trans_lt h
+  exact ⟨this h.1, this h.2⟩
+
+theorem hausdorffEdist_le_of_mem_hausdorffEntourage {s t : Set α} {δ : ℝ≥0∞}
+    (h : (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 ≤ δ}) : hausdorffEdist s t ≤ δ := by
+  rw [hausdorffEdist, max_le_iff]
+  rw [hausdorffEntourage, Set.mem_setOf] at h
+  conv at h => enter [2, 2, 1, 1, _]; rw [edist_comm]
+  have {s t : Set α} (h : s ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} t) :
+      ⨆ x ∈ s, infEdist x t ≤ δ := by
+    rw [iSup₂_le_iff]
+    intro x hx
+    obtain ⟨y, hy, hxy⟩ := h hx
+    exact iInf₂_le_of_le y hy hxy
+  exact ⟨this h.1, this h.2⟩
+
+/-- The Hausdorff pseudo emetric on the powerset of a pseudo emetric space.
+See note [reducible non-instances]. -/
+protected abbrev _root_.PseudoEMetricSpace.hausdorff : PseudoEMetricSpace (Set α) where
+  edist s t := hausdorffEdist s t
+  edist_self _ := hausdorffEdist_self
+  edist_comm _ _ := hausdorffEdist_comm
+  edist_triangle _ _ _ := hausdorffEdist_triangle
+  toUniformSpace := .hausdorff α
+  uniformity_edist := by
+    refine le_antisymm
+      (le_iInf₂ fun ε hε => Filter.le_principal_iff.mpr ?_)
+      (uniformity_basis_edist.lift' monotone_hausdorffEntourage |>.ge_iff.mpr fun ε hε =>
+        Filter.mem_iInf_of_mem ε <| Filter.mem_iInf_of_mem hε fun _ =>
+        mem_hausdorffEntourage_of_hausdorffEdist_lt)
+    obtain ⟨δ, hδ, hδε⟩ := exists_between hε
+    filter_upwards [Filter.mem_lift' (uniformity_basis_edist_le.mem_of_mem hδ)]
+      with _ h using hδε.trans_le' <| hausdorffEdist_le_of_mem_hausdorffEntourage h
+
+end
+
+section
+
 variable {α β : Type*} [EMetricSpace α] [EMetricSpace β] {s : Set α}
 
 /-- In emetric spaces, the Hausdorff edistance defines an emetric space structure
 on the type of closed subsets -/
 instance Closeds.emetricSpace : EMetricSpace (Closeds α) where
-  edist s t := hausdorffEdist (s : Set α) t
-  edist_self _ := hausdorffEdist_self
-  edist_comm _ _ := hausdorffEdist_comm
-  edist_triangle _ _ _ := hausdorffEdist_triangle
+  __ := PseudoEMetricSpace.hausdorff.induced SetLike.coe
   eq_of_edist_eq_zero {s t} h :=
     Closeds.ext <| (hausdorffEdist_zero_iff_eq_of_closed s.isClosed t.isClosed).1 h
 
@@ -63,20 +108,11 @@ theorem continuous_infEdist_hausdorffEdist :
     _ = infEdist y t + 2 * edist (x, s) (y, t) := by rw [← mul_two, mul_comm]
 
 /-- Subsets of a given closed subset form a closed set -/
-theorem Closeds.isClosed_subsets_of_isClosed (hs : IsClosed s) :
-    IsClosed { t : Closeds α | (t : Set α) ⊆ s } := by
-  refine isClosed_of_closure_subset fun
-    (t : Closeds α) (ht : t ∈ closure {t : Closeds α | (t : Set α) ⊆ s}) (x : α) (hx : x ∈ t) => ?_
-  have : x ∈ closure s := by
-    refine mem_closure_iff.2 fun ε εpos => ?_
-    obtain ⟨u : Closeds α, hu : u ∈ {t : Closeds α | (t : Set α) ⊆ s}, Dtu : edist t u < ε⟩ :=
-      mem_closure_iff.1 ht ε εpos
-    obtain ⟨y : α, hy : y ∈ u, Dxy : edist x y < ε⟩ := exists_edist_lt_of_hausdorffEdist_lt hx Dtu
-    exact ⟨y, hu hy, Dxy⟩
-  rwa [hs.closure_eq] at this
+@[deprecated (since := "2025-11-19")]
+alias Closeds.isClosed_subsets_of_isClosed := TopologicalSpace.Closeds.isClosed_subsets_of_isClosed
 
 @[deprecated (since := "2025-08-20")]
-alias isClosed_subsets_of_isClosed := Closeds.isClosed_subsets_of_isClosed
+alias isClosed_subsets_of_isClosed := TopologicalSpace.Closeds.isClosed_subsets_of_isClosed
 
 /-- By definition, the edistance on `Closeds α` is given by the Hausdorff edistance -/
 theorem Closeds.edist_eq {s t : Closeds α} : edist s t = hausdorffEdist (s : Set α) t :=
@@ -235,10 +271,7 @@ 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
-  edist s t := hausdorffEdist (s : Set α) t
-  edist_self _ := hausdorffEdist_self
-  edist_comm _ _ := hausdorffEdist_comm
-  edist_triangle _ _ _ := hausdorffEdist_triangle
+  __ := PseudoEMetricSpace.hausdorff.induced SetLike.coe
   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
@@ -248,21 +281,18 @@ theorem isometry_toCloseds : Isometry (@NonemptyCompacts.toCloseds α _ _) :=
   fun _ _ => rfl
 
 /-- `NonemptyCompacts.toCloseds` is a uniform embedding (as it is an isometry) -/
-theorem isUniformEmbedding_toCloseds :
-    IsUniformEmbedding (@NonemptyCompacts.toCloseds α _ _) :=
-  isometry_toCloseds.isUniformEmbedding
+@[deprecated (since := "2025-11-19")]
+alias isUniformEmbedding_toCloseds := TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds
 
 @[deprecated (since := "2025-08-20")]
-alias ToCloseds.isUniformEmbedding := isUniformEmbedding_toCloseds
+alias ToCloseds.isUniformEmbedding := TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds
 
 /-- `NonemptyCompacts.toCloseds` is continuous (as it is an isometry) -/
-@[fun_prop]
-theorem continuous_toCloseds : Continuous (@NonemptyCompacts.toCloseds α _ _) :=
-  isometry_toCloseds.continuous
+@[deprecated (since := "2025-11-19")]
+alias continuous_toCloseds := TopologicalSpace.NonemptyCompacts.continuous_toCloseds
 
-lemma isClosed_subsets_of_isClosed (hs : IsClosed s) :
-    IsClosed {A : NonemptyCompacts α | (A : Set α) ⊆ s} :=
-  (Closeds.isClosed_subsets_of_isClosed hs).preimage continuous_toCloseds
+@[deprecated (since := "2025-11-19")]
+alias isClosed_subsets_of_isClosed := TopologicalSpace.NonemptyCompacts.isClosed_subsets_of_isClosed
 
 /-- The range of `NonemptyCompacts.toCloseds` is closed in a complete space -/
 theorem isClosed_in_closeds [CompleteSpace α] :

Mathlib/Topology/Order.lean

@@ -813,6 +813,10 @@ theorem isOpen_induced_eq {s : Set α} :
 theorem isOpen_induced {s : Set β} (h : IsOpen s) : IsOpen[induced f t] (f ⁻¹' s) :=
   ⟨s, h, rfl⟩
 
+theorem isClosed_induced {s : Set β} (h : IsClosed s) : IsClosed[induced f t] (f ⁻¹' s) := by
+  simp_rw [← isOpen_compl_iff]
+  exact isOpen_induced h.isOpen_compl
+
 theorem map_nhds_induced_eq (a : α) : map f (@nhds α (induced f t) a) = 𝓝[range f] f a := by
   rw [nhds_induced, Filter.map_comap, nhdsWithin]
 

Mathlib/Topology/Sets/Compacts.lean

@@ -67,6 +67,9 @@ theorem mem_toCloseds [T2Space α] {x : α} {s : Compacts α} :
     x ∈ s.toCloseds ↔ x ∈ s :=
   Iff.rfl
 
+theorem toCloseds_injective [T2Space α] : Function.Injective (toCloseds (α := α)) :=
+  .of_comp (f := SetLike.coe) SetLike.coe_injective
+
 instance : CanLift (Set α) (Compacts α) (↑) IsCompact where prf K hK := ⟨⟨K, hK⟩, rfl⟩
 
 @[ext]
@@ -295,6 +298,9 @@ theorem mem_toCloseds [T2Space α] {x : α} {s : NonemptyCompacts α} :
     x ∈ s.toCloseds ↔ x ∈ s :=
   Iff.rfl
 
+theorem toCloseds_injective [T2Space α] : Function.Injective (toCloseds (α := α)) :=
+  .of_comp (f := SetLike.coe) SetLike.coe_injective
+
 @[ext]
 protected theorem ext {s t : NonemptyCompacts α} (h : (s : Set α) = t) : s = t :=
   SetLike.ext' h
@@ -314,6 +320,9 @@ theorem mem_toCompacts {x : α} {s : NonemptyCompacts α} :
     x ∈ s.toCompacts ↔ x ∈ s :=
   Iff.rfl
 
+theorem toCompacts_injective : Function.Injective (toCompacts (α := α)) :=
+  .of_comp (f := SetLike.coe) SetLike.coe_injective
+
 instance : Max (NonemptyCompacts α) :=
   ⟨fun s t => ⟨s.toCompacts ⊔ t.toCompacts, s.nonempty.mono subset_union_left⟩⟩