feat: minor topological improvements (#9908)

* Prove that a set is a Gdelta if and only if it is an intersection of open sets indexed by `ℕ`.
* Cleanup porting todos in the Gdelta file
* Rename `cluster_point_of_compact` to `exists_clusterPt_of_compactSpace `
* Generalize the class `T2Space` to `T2OrLocallyCompactRegularSpace` in the file `Support.lean`

Author: sgouezel

Mathlib/Data/ENNReal/Operations.lean

@@ -472,6 +472,10 @@ theorem mul_sub (h : 0 < c → c < b → a ≠ ∞) : a * (b - c) = a * b - a *
   exact sub_mul h
 #align ennreal.mul_sub ENNReal.mul_sub
 
+theorem sub_le_sub_iff_left (h : c ≤ a) (h' : a ≠ ∞) :
+    (a - b ≤ a - c) ↔ c ≤ b :=
+  (cancel_of_ne h').tsub_le_tsub_iff_left (cancel_of_ne (ne_top_of_le_ne_top h' h)) h
+
 end Sub
 
 section Sum

Mathlib/Topology/Compactness/Compact.lean

@@ -43,6 +43,13 @@ def IsCompact (s : Set X) :=
   ∀ ⦃f⦄ [NeBot f], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f
 #align is_compact IsCompact
 
+lemma IsCompact.exists_clusterPt (hs : IsCompact s) {f : Filter X} [NeBot f] (hf : f ≤ 𝓟 s) :
+    ∃ x ∈ s, ClusterPt x f := hs hf
+
+lemma IsCompact.exists_mapClusterPt {ι : Type*} (hs : IsCompact s) {f : Filter ι} [NeBot f]
+    {u : ι → X} (hf : Filter.map u f ≤ 𝓟 s) :
+    ∃ x ∈ s, MapClusterPt x f u := hs hf
+
 /-- The complement to a compact set belongs to a filter `f` if it belongs to each filter
 `𝓝 x ⊓ f`, `x ∈ s`. -/
 theorem IsCompact.compl_mem_sets (hs : IsCompact s) {f : Filter X} (hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f) :
@@ -708,9 +715,13 @@ theorem isCompact_univ [h : CompactSpace X] : IsCompact (univ : Set X) :=
   h.isCompact_univ
 #align is_compact_univ isCompact_univ
 
-theorem cluster_point_of_compact [CompactSpace X] (f : Filter X) [NeBot f] : ∃ x, ClusterPt x f :=
+theorem exists_clusterPt_of_compactSpace [CompactSpace X] (f : Filter X) [NeBot f] :
+    ∃ x, ClusterPt x f :=
   by simpa using isCompact_univ (show f ≤ 𝓟 univ by simp)
-#align cluster_point_of_compact cluster_point_of_compact
+#align cluster_point_of_compact exists_clusterPt_of_compactSpace
+
+@[deprecated] -- Since 28 January 2024
+alias cluster_point_of_compact := exists_clusterPt_of_compactSpace
 
 nonrec theorem Ultrafilter.le_nhds_lim [CompactSpace X] (F : Ultrafilter X) : ↑F ≤ 𝓝 F.lim := by
   rcases isCompact_univ.ultrafilter_le_nhds F (by simp) with ⟨x, -, h⟩

Mathlib/Topology/GDelta.lean

@@ -45,8 +45,9 @@ Gδ set, residual set, nowhere dense set, meagre set
 noncomputable section
 
 open Topology TopologicalSpace Filter Encodable Set
+open scoped Uniformity
 
-variable {X Y ι : Type*}
+variable {X Y ι : Type*} {ι' : Sort*}
 
 set_option linter.uppercaseLean3 false
 
@@ -79,19 +80,28 @@ theorem isGδ_biInter_of_isOpen {I : Set ι} (hI : I.Countable) {f : ι → Set
   ⟨f '' I, by rwa [ball_image_iff], hI.image _, by rw [sInter_image]⟩
 #align is_Gδ_bInter_of_open isGδ_biInter_of_isOpen
 
--- porting note: TODO: generalize to `Sort*` + `Countable _`
-theorem isGδ_iInter_of_isOpen [Encodable ι] {f : ι → Set X} (hf : ∀ i, IsOpen (f i)) :
+theorem isGδ_iInter_of_isOpen [Countable ι'] {f : ι' → Set X} (hf : ∀ i, IsOpen (f i)) :
     IsGδ (⋂ i, f i) :=
   ⟨range f, by rwa [forall_range_iff], countable_range _, by rw [sInter_range]⟩
 #align is_Gδ_Inter_of_open isGδ_iInter_of_isOpen
 
--- porting note: TODO: generalize to `Sort*` + `Countable _`
+lemma isGδ_iff_eq_iInter_nat {s : Set X} :
+    IsGδ s ↔ ∃ (f : ℕ → Set X), (∀ n, IsOpen (f n)) ∧ s = ⋂ n, f n := by
+  refine ⟨?_, ?_⟩
+  · rintro ⟨T, hT, T_count, rfl⟩
+    rcases Set.eq_empty_or_nonempty T with rfl|hT
+    · exact ⟨fun _n ↦ univ, fun _n ↦ isOpen_univ, by simp⟩
+    · obtain ⟨f, hf⟩ : ∃ (f : ℕ → Set X), T = range f := Countable.exists_eq_range T_count hT
+      exact ⟨f, by aesop, by simp [hf]⟩
+  · rintro ⟨f, hf, rfl⟩
+    apply isGδ_iInter_of_isOpen hf
+
 /-- The intersection of an encodable family of Gδ sets is a Gδ set. -/
-theorem isGδ_iInter [Encodable ι] {s : ι → Set X} (hs : ∀ i, IsGδ (s i)) : IsGδ (⋂ i, s i) := by
+theorem isGδ_iInter [Countable ι'] {s : ι' → Set X} (hs : ∀ i, IsGδ (s i)) : IsGδ (⋂ i, s i) := by
   choose T hTo hTc hTs using hs
   obtain rfl : s = fun i => ⋂₀ T i := funext hTs
   refine' ⟨⋃ i, T i, _, countable_iUnion hTc, (sInter_iUnion _).symm⟩
-  simpa [@forall_swap ι] using hTo
+  simpa [@forall_swap ι'] using hTo
 #align is_Gδ_Inter isGδ_iInter
 
 theorem isGδ_biInter {s : Set ι} (hs : s.Countable) {t : ∀ i ∈ s, Set X}
@@ -130,8 +140,7 @@ theorem isGδ_biUnion {s : Set ι} (hs : s.Finite) {f : ι → Set X} (h : ∀ i
   exact fun _ _ ihs H => H.1.union (ihs H.2)
 #align is_Gδ_bUnion isGδ_biUnion
 
--- Porting note: Did not recognize notation 𝓤 X, needed to replace with uniformity X
-theorem IsClosed.isGδ {X} [UniformSpace X] [IsCountablyGenerated (uniformity X)] {s : Set X}
+theorem IsClosed.isGδ {X} [UniformSpace X] [IsCountablyGenerated (𝓤 X)] {s : Set X}
     (hs : IsClosed s) : IsGδ s := by
   rcases (@uniformity_hasBasis_open X _).exists_antitone_subbasis with ⟨U, hUo, hU, -⟩
   rw [← hs.closure_eq, ← hU.biInter_biUnion_ball]
@@ -185,7 +194,7 @@ section ContinuousAt
 variable [TopologicalSpace X]
 
 /-- The set of points where a function is continuous is a Gδ set. -/
-theorem isGδ_setOf_continuousAt [UniformSpace Y] [IsCountablyGenerated (uniformity Y)] (f : X → Y) :
+theorem isGδ_setOf_continuousAt [UniformSpace Y] [IsCountablyGenerated (𝓤 Y)] (f : X → Y) :
     IsGδ { x | ContinuousAt f x } := by
   obtain ⟨U, _, hU⟩ := (@uniformity_hasBasis_open_symmetric Y _).exists_antitone_subbasis
   simp only [Uniform.continuousAt_iff_prod, nhds_prod_eq]

Mathlib/Topology/Support.lean

@@ -165,7 +165,7 @@ theorem hasCompactMulSupport_def : HasCompactMulSupport f ↔ IsCompact (closure
 #align has_compact_support_def hasCompactSupport_def
 
 @[to_additive]
-theorem exists_compact_iff_hasCompactMulSupport [T2Space α] :
+theorem exists_compact_iff_hasCompactMulSupport [T2OrLocallyCompactRegularSpace α] :
     (∃ K : Set α, IsCompact K ∧ ∀ x, x ∉ K → f x = 1) ↔ HasCompactMulSupport f := by
   simp_rw [← nmem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl,
     hasCompactMulSupport_def, exists_compact_superset_iff]
@@ -174,7 +174,7 @@ theorem exists_compact_iff_hasCompactMulSupport [T2Space α] :
 
 namespace HasCompactMulSupport
 @[to_additive]
-theorem intro [T2Space α] {K : Set α} (hK : IsCompact K)
+theorem intro [T2OrLocallyCompactRegularSpace α] {K : Set α} (hK : IsCompact K)
     (hfK : ∀ x, x ∉ K → f x = 1) : HasCompactMulSupport f :=
   exists_compact_iff_hasCompactMulSupport.mp ⟨K, hK, hfK⟩
 #align has_compact_mul_support.intro HasCompactMulSupport.intro
@@ -189,8 +189,8 @@ theorem intro' {K : Set α} (hK : IsCompact K) (h'K : IsClosed K)
   exact IsCompact.of_isClosed_subset hK ( isClosed_mulTSupport f) this
 
 @[to_additive]
-theorem of_mulSupport_subset_isCompact [T2Space α] {K : Set α}
-    (hK : IsCompact K) (h : mulSupport f ⊆ K) : HasCompactMulSupport f :=
+theorem of_mulSupport_subset_isCompact [T2OrLocallyCompactRegularSpace α]
+    {K : Set α} (hK : IsCompact K) (h : mulSupport f ⊆ K) : HasCompactMulSupport f :=
   isCompact_closure_of_subset_compact hK h
 
 @[to_additive]
@@ -272,6 +272,14 @@ theorem comp₂_left (hf : HasCompactMulSupport f)
 #align has_compact_mul_support.comp₂_left HasCompactMulSupport.comp₂_left
 #align has_compact_support.comp₂_left HasCompactSupport.comp₂_left
 
+@[to_additive]
+lemma isCompact_preimage [TopologicalSpace β]
+    (h'f : HasCompactMulSupport f) (hf : Continuous f) {k : Set β} (hk : IsClosed k)
+    (h'k : 1 ∉ k) : IsCompact (f ⁻¹' k) := by
+  apply IsCompact.of_isClosed_subset h'f (hk.preimage hf) (fun x hx ↦ ?_)
+  apply subset_mulTSupport
+  aesop
+
 variable [T2Space α'] (hf : HasCompactMulSupport f) {g : α → α'} (cont : Continuous g)
 
 @[to_additive]

Mathlib/Topology/UniformSpace/Compact.lean

@@ -94,7 +94,7 @@ def uniformSpaceOfCompactT2 [TopologicalSpace γ] [CompactSpace γ] [T2Space γ]
     by_contra H
     haveI : NeBot (F ⊓ 𝓟 Vᶜ) := ⟨H⟩
     -- Hence compactness would give us a cluster point (x, y) for F ⊓ 𝓟 Vᶜ
-    obtain ⟨⟨x, y⟩, hxy⟩ : ∃ p : γ × γ, ClusterPt p (F ⊓ 𝓟 Vᶜ) := cluster_point_of_compact _
+    obtain ⟨⟨x, y⟩, hxy⟩ : ∃ p : γ × γ, ClusterPt p (F ⊓ 𝓟 Vᶜ) := exists_clusterPt_of_compactSpace _
     -- In particular (x, y) is a cluster point of 𝓟 Vᶜ, hence is not in the interior of V,
     -- and a fortiori not in Δ, so x ≠ y
     have clV : ClusterPt (x, y) (𝓟 <| Vᶜ) := hxy.of_inf_right