chore: rename RestrictGenTopology to Topology.IsCoherentWith (#18397)

Rename `Topology.RestrictGenTopology` to `Topology.IsCoherentWith` since
* the `Topology` part is understood
* the name should be prefixed with `Is` to show it's Prop-valued
* "coherent topology" is the informal name for this notion: https://en.wikipedia.org/wiki/Coherent_topology



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: YaelDillies

Mathlib.lean

@@ -5846,6 +5846,7 @@ import Mathlib.Topology.Clopen
 import Mathlib.Topology.ClopenBox
 import Mathlib.Topology.Closure
 import Mathlib.Topology.ClusterPt
+import Mathlib.Topology.Coherent
 import Mathlib.Topology.CompactOpen
 import Mathlib.Topology.Compactification.OnePoint
 import Mathlib.Topology.Compactification.OnePointEquiv
@@ -6091,7 +6092,6 @@ import Mathlib.Topology.Perfect
 import Mathlib.Topology.Piecewise
 import Mathlib.Topology.PreorderRestrict
 import Mathlib.Topology.QuasiSeparated
-import Mathlib.Topology.RestrictGen
 import Mathlib.Topology.Semicontinuous
 import Mathlib.Topology.SeparatedMap
 import Mathlib.Topology.Separation.Basic

Mathlib/Topology/Algebra/Module/Alternating/Topology.lean

@@ -89,7 +89,7 @@ section CompleteSpace
 variable [ContinuousSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] [CompleteSpace F]
 
 open UniformOnFun in
-theorem completeSpace (h : RestrictGenTopology {s : Set (ι → E) | IsVonNBounded 𝕜 s}) :
+theorem completeSpace (h : IsCoherentWith {s : Set (ι → E) | IsVonNBounded 𝕜 s}) :
     CompleteSpace (E [⋀^ι]→L[𝕜] F) := by
   wlog hF : T2Space F generalizing F
   · rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)

Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

@@ -120,7 +120,7 @@ section CompleteSpace
 variable [∀ i, ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] [CompleteSpace F]
 
 open UniformOnFun in
-theorem completeSpace (h : RestrictGenTopology {s : Set (Π i, E i) | IsVonNBounded 𝕜 s}) :
+theorem completeSpace (h : IsCoherentWith {s : Set (Π i, E i) | IsVonNBounded 𝕜 s}) :
     CompleteSpace (ContinuousMultilinearMap 𝕜 E F) := by
   classical
   wlog hF : T2Space F generalizing F

Mathlib/Topology/Algebra/Module/StrongTopology.lean

@@ -301,7 +301,7 @@ theorem isUniformInducing_postcomp
   exact (UniformOnFun.postcomp_isUniformInducing hg).comp (isUniformInducing_coeFn _ _ _)
 
 theorem completeSpace [UniformSpace F] [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F]
-    {𝔖 : Set (Set E)} (h𝔖 : RestrictGenTopology 𝔖) (h𝔖U : ⋃₀ 𝔖 = univ) :
+    {𝔖 : Set (Set E)} (h𝔖 : IsCoherentWith 𝔖) (h𝔖U : ⋃₀ 𝔖 = univ) :
     CompleteSpace (UniformConvergenceCLM σ F 𝔖) := by
   wlog hF : T2Space F generalizing F
   · rw [(isUniformInducing_postcomp σ (SeparationQuotient.mkCLM 𝕜₂ F)
@@ -452,7 +452,7 @@ theorem isVonNBounded_iff {R : Type*} [NormedDivisionRing R]
   UniformConvergenceCLM.isVonNBounded_iff
 
 theorem completeSpace [UniformSpace F] [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F]
-    [ContinuousSMul 𝕜₁ E] (h : RestrictGenTopology {s : Set E | IsVonNBounded 𝕜₁ s}) :
+    [ContinuousSMul 𝕜₁ E] (h : IsCoherentWith {s : Set E | IsVonNBounded 𝕜₁ s}) :
     CompleteSpace (E →SL[σ] F) :=
   UniformConvergenceCLM.completeSpace _ _ h isVonNBounded_covers
 

Mathlib/Topology/RestrictGen.lean renamed to Mathlib/Topology/Coherent.lean

@@ -19,56 +19,56 @@ if either of the following equivalent conditions hold:
   provided that it is continuous on each `s ∈ S`.
 
 We use the first condition as the definition
-(see `RestrictGenTopology` in `Mathlib/Topology/Defs/Induced.lean`),
+(see `IsCoherentWith` in `Mathlib/Topology/Defs/Induced.lean`),
 and provide the others as corollaries.
 
 ## Main results
 
-- `RestrictGenTopology.of_seq`: if `X` is a sequential space
+- `IsCoherentWith.of_seq`: if `X` is a sequential space
   and `S` contains all sets of the form `insert x (Set.range u)`,
   where `u : ℕ → X` is a sequence that converges to `x`,
-  then we have `RestrictGenTopology S`;
+  then we have `IsCoherentWith S`;
 
-- `RestrictGenTopology.isCompact_of_seq`: specialization of the previous lemma
+- `IsCoherentWith.isCompact_of_seq`: specialization of the previous lemma
   to the case `S = {K | IsCompact K}`.
 -/
 
 open Filter Set
 
 variable {X : Type*} [TopologicalSpace X] {S : Set (Set X)} {t : Set X} {x : X}
 
-namespace Topology.RestrictGenTopology
+namespace Topology.IsCoherentWith
 
-protected theorem isOpen_iff (hS : RestrictGenTopology S) :
+protected theorem isOpen_iff (hS : IsCoherentWith S) :
     IsOpen t ↔ ∀ s ∈ S, IsOpen ((↑) ⁻¹' t : Set s) :=
   ⟨fun ht _ _ ↦ ht.preimage continuous_subtype_val, hS.1 t⟩
 
-protected theorem isClosed_iff (hS : RestrictGenTopology S) :
+protected theorem isClosed_iff (hS : IsCoherentWith S) :
     IsClosed t ↔ ∀ s ∈ S, IsClosed ((↑) ⁻¹' t : Set s) := by
   simp only [← isOpen_compl_iff, hS.isOpen_iff, preimage_compl]
 
 protected theorem continuous_iff {Y : Type*} [TopologicalSpace Y] {f : X → Y}
-    (hS : RestrictGenTopology S) :
+    (hS : IsCoherentWith S) :
     Continuous f ↔ ∀ s ∈ S, ContinuousOn f s :=
   ⟨fun h _ _ ↦ h.continuousOn, fun h ↦ continuous_def.2 fun _u hu ↦ hS.isOpen_iff.2 fun s hs ↦
     hu.preimage <| (h s hs).restrict⟩
 
 theorem of_continuous_prop (h : ∀ f : X → Prop, (∀ s ∈ S, ContinuousOn f s) → Continuous f) :
-    RestrictGenTopology S where
+    IsCoherentWith S where
   isOpen_of_forall_induced u hu := by
     simp only [continuousOn_iff_continuous_restrict, continuous_Prop] at *
     exact h _ hu
 
 theorem of_isClosed (h : ∀ t : Set X, (∀ s ∈ S, IsClosed ((↑) ⁻¹' t : Set s)) → IsClosed t) :
-    RestrictGenTopology S :=
+    IsCoherentWith S :=
   ⟨fun _t ht ↦ isClosed_compl_iff.1 <| h _ fun s hs ↦ (ht s hs).isClosed_compl⟩
 
-protected theorem enlarge {T} (hS : RestrictGenTopology S) (hT : ∀ s ∈ S, ∃ t ∈ T, s ⊆ t) :
-    RestrictGenTopology T :=
+protected theorem enlarge {T} (hS : IsCoherentWith S) (hT : ∀ s ∈ S, ∃ t ∈ T, s ⊆ t) :
+    IsCoherentWith T :=
   of_continuous_prop fun _f hf ↦ hS.continuous_iff.2 fun s hs ↦
     let ⟨t, htT, hst⟩ := hT s hs; (hf t htT).mono hst
 
-protected theorem mono {T} (hS : RestrictGenTopology S) (hT : S ⊆ T) : RestrictGenTopology T :=
+protected theorem mono {T} (hS : IsCoherentWith S) (hT : S ⊆ T) : IsCoherentWith T :=
   hS.enlarge fun s hs ↦ ⟨s, hT hs, Subset.rfl⟩
 
 /-- If `X` is a sequential space
@@ -77,7 +77,7 @@ where `u : ℕ → X` is a sequence and `x` is its limit,
 then topology on `X` is generated by its restrictions to the sets of `S`. -/
 lemma of_seq [SequentialSpace X]
     (h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S) :
-    RestrictGenTopology S := by
+    IsCoherentWith S := by
   refine of_isClosed fun t ht ↦ IsSeqClosed.isClosed fun u x hut hux ↦ ?_
   rcases isClosed_induced_iff.1 (ht _ (h hux)) with ⟨s, hsc, hst⟩
   rw [Subtype.preimage_val_eq_preimage_val_iff, Set.ext_iff] at hst
@@ -87,19 +87,19 @@ lemma of_seq [SequentialSpace X]
   simp_all
 
 /-- A sequential space is compactly generated. -/
-lemma isCompact_of_seq [SequentialSpace X] : RestrictGenTopology {K : Set X | IsCompact K} :=
+lemma isCompact_of_seq [SequentialSpace X] : IsCoherentWith {K : Set X | IsCompact K} :=
   of_seq fun _u _x hux ↦ hux.isCompact_insert_range
 
 /-- If each point of the space has a neighborhood from the family `S`,
 then the topology is generated by its restrictions to the sets of `S`. -/
-lemma of_nhds (h : ∀ x, ∃ s ∈ S, s ∈ 𝓝 x) : RestrictGenTopology S :=
+lemma of_nhds (h : ∀ x, ∃ s ∈ S, s ∈ 𝓝 x) : IsCoherentWith S :=
   of_continuous_prop fun _f hf ↦ continuous_iff_continuousAt.2 fun x ↦
     let ⟨s, hsS, hsx⟩ := h x
     (hf s hsS).continuousAt hsx
 
 /-- A weakly locally compact space is compactly generated. -/
 lemma isCompact_of_weaklyLocallyCompact [WeaklyLocallyCompactSpace X] :
-    RestrictGenTopology {K : Set X | IsCompact K} :=
+    IsCoherentWith {K : Set X | IsCompact K} :=
   of_nhds exists_compact_mem_nhds
 
-end Topology.RestrictGenTopology
+end Topology.IsCoherentWith

Mathlib/Topology/Defs/Induced.lean

@@ -93,9 +93,11 @@ if either of the following equivalent conditions hold:
 - for any topological space `Y`, a function `f : X → Y` is continuous
   provided that it is continuous on each `s ∈ S`.
 -/
-structure RestrictGenTopology (S : Set (Set X)) : Prop where
+structure IsCoherentWith (S : Set (Set X)) : Prop where
   isOpen_of_forall_induced (u : Set X) : (∀ s ∈ S, IsOpen ((↑) ⁻¹' u : Set s)) → IsOpen u
 
+@[deprecated (since := "2025-04-08")] alias RestrictGenTopology := Topology.IsCoherentWith
+
 /-- A function `f : X → Y` between topological spaces is inducing if the topology on `X` is induced
 by the topology on `Y` through `f`, meaning that a set `s : Set X` is open iff it is the preimage
 under `f` of some open set `t : Set Y`. -/

Mathlib/Topology/UniformSpace/CompactConvergence.lean

@@ -85,7 +85,7 @@ so that the resulting instance uses the compact-open topology.
 -/
 
 open Filter Set Topology UniformSpace
-open scoped Uniformity Topology UniformConvergence
+open scoped Uniformity UniformConvergence
 
 universe u₁ u₂ u₃
 variable {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β]
@@ -375,20 +375,21 @@ continuous maps `C(α, β)` is complete (wrt the compact convergence uniformity)
 Sufficient conditions on `α` to satisfy this condition are (weak) local compactness (see
 `ContinuousMap.instCompleteSpaceOfWeaklyLocallyCompactSpace`) and sequential compactness (see
 `ContinuousMap.instCompleteSpaceOfSequentialSpace`). -/
-lemma completeSpace_of_restrictGenTopology (h : RestrictGenTopology {K : Set α | IsCompact K}) :
+lemma completeSpace_of_isCoherentWith (h : IsCoherentWith {K : Set α | IsCompact K}) :
     CompleteSpace C(α, β) := by
   rw [completeSpace_iff_isComplete_range
     isUniformEmbedding_toUniformOnFunIsCompact.isUniformInducing,
     range_toUniformOnFunIsCompact, ← completeSpace_coe_iff_isComplete]
   exact (UniformOnFun.isClosed_setOf_continuous h).completeSpace_coe
 
+@[deprecated (since := "2025-04-08")]
+alias completeSpace_of_restrictGenTopology := completeSpace_of_isCoherentWith
+
 instance instCompleteSpaceOfWeaklyLocallyCompactSpace [WeaklyLocallyCompactSpace α] :
-    CompleteSpace C(α, β) :=
-  completeSpace_of_restrictGenTopology RestrictGenTopology.isCompact_of_weaklyLocallyCompact
+    CompleteSpace C(α, β) := completeSpace_of_isCoherentWith .isCompact_of_weaklyLocallyCompact
 
 instance instCompleteSpaceOfSequentialSpace [SequentialSpace α] :
-    CompleteSpace C(α, β) :=
-  completeSpace_of_restrictGenTopology RestrictGenTopology.isCompact_of_seq
+    CompleteSpace C(α, β) := completeSpace_of_isCoherentWith .isCompact_of_seq
 
 end CompleteSpace
 

Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

@@ -6,7 +6,7 @@ Authors: Anatole Dedecker
 import Mathlib.Topology.UniformSpace.UniformConvergence
 import Mathlib.Topology.UniformSpace.Pi
 import Mathlib.Topology.UniformSpace.Equiv
-import Mathlib.Topology.RestrictGen
+import Mathlib.Topology.Coherent
 
 /-!
 # Topology and uniform structure of uniform convergence
@@ -1059,7 +1059,7 @@ protected def uniformEquivPiComm : (α →ᵤ[𝔖] ((i : ι) → δ i)) ≃ᵤ
 
 Then the set of continuous functions is closed
 in the topology of uniform convergence on the sets of `𝔖`. -/
-theorem isClosed_setOf_continuous [TopologicalSpace α] (h : RestrictGenTopology 𝔖) :
+theorem isClosed_setOf_continuous [TopologicalSpace α] (h : IsCoherentWith 𝔖) :
     IsClosed {f : α →ᵤ[𝔖] β | Continuous (toFun 𝔖 f)} := by
   refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ h.continuous_iff.2 fun s hs ↦ ?_
   rw [← tendsto_id', UniformOnFun.tendsto_iff_tendstoUniformlyOn] at huf