feat: define RestrictGenTopology (#13452)

Mathlib.lean

@@ -4346,6 +4346,7 @@ import Mathlib.Topology.PartitionOfUnity
 import Mathlib.Topology.Perfect
 import Mathlib.Topology.ProperMap
 import Mathlib.Topology.QuasiSeparated
+import Mathlib.Topology.RestrictGenTopology
 import Mathlib.Topology.Semicontinuous
 import Mathlib.Topology.SeparatedMap
 import Mathlib.Topology.Separation

Mathlib/Topology/Constructions.lean

@@ -44,10 +44,6 @@ variable {X : Type u} {Y : Type v} {Z W ε ζ : Type*}
 
 section Constructions
 
-instance instTopologicalSpaceSubtype {p : X → Prop} [t : TopologicalSpace X] :
-    TopologicalSpace (Subtype p) :=
-  induced (↑) t
-
 instance {r : X → X → Prop} [t : TopologicalSpace X] : TopologicalSpace (Quot r) :=
   coinduced (Quot.mk r) t
 

Mathlib/Topology/Defs/Induced.lean

@@ -42,6 +42,7 @@ as well as topology inducing maps, topological embeddings, and quotient maps.
 -/
 
 open Set
+open scoped Topology
 
 namespace TopologicalSpace
 
@@ -64,6 +65,10 @@ def induced (f : X → Y) (t : TopologicalSpace Y) : TopologicalSpace X where
     exact iUnion₂_congr hfg
 #align topological_space.induced TopologicalSpace.induced
 
+instance _root_.instTopologicalSpaceSubtype {p : X → Prop} [t : TopologicalSpace X] :
+    TopologicalSpace (Subtype p) :=
+  induced (↑) t
+
 /-- Given `f : X → Y` and a topology on `X`,
   the coinduced topology on `Y` is defined such that
   `s : Set Y` is open if the preimage of `s` is open.
@@ -79,6 +84,18 @@ end TopologicalSpace
 
 variable {X Y : Type*} [tX : TopologicalSpace X] [tY : TopologicalSpace Y]
 
+/-- We say that restrictions of the topology on `X` to sets from a family `S`
+generates the original topology,
+if either of the following equivalent conditions hold:
+
+- a set which is relatively open in each `s ∈ S` is open;
+- a set which is relatively closed in each `s ∈ S` is closed;
+- 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
+  isOpen_of_forall_induced (u : Set X) : (∀ s ∈ S, IsOpen ((↑) ⁻¹' u : Set s)) → IsOpen u
+
 /-- 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/RestrictGenTopology.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2024 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Topology.Defs.Sequences
+import Mathlib.Topology.Compactness.Compact
+
+/-!
+# Topology generated by its restrictions to subsets
+
+We say that restrictions of the topology on `X` to sets from a family `S`
+generates the original topology,
+if either of the following equivalent conditions hold:
+
+- a set which is relatively open in each `s ∈ S` is open;
+- a set which is relatively closed in each `s ∈ S` is closed;
+- for any topological space `Y`, a function `f : X → Y` is continuous
+  provided that it is continuous on each `s ∈ S`.
+
+We use the first condition as the definition
+(see `RestrictGenTopology` in `Topology/Defs/Induced.lean`),
+and provide the others as corollaries.
+
+## Main results
+
+- `RestrictGenTopology.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`;
+
+- `RestrictGenTopology.isCompact_of_seq`: specialization of the previous lemma
+  to the case `S = {K | IsCompact K}`.
+-/
+
+open Set Filter
+open scoped Topology
+
+variable {X : Type*} [TopologicalSpace X] {S : Set (Set X)} {t : Set X} {x : X}
+
+namespace RestrictGenTopology
+
+protected theorem isOpen_iff (hS : RestrictGenTopology 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) :
+    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) :
+    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
+  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 :=
+  ⟨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 :=
+  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 :=
+  hS.enlarge fun s hs ↦ ⟨s, hT hs, Subset.rfl⟩
+
+/-- If `X` is a sequential space
+and `S` contains each set of the form `insert x (Set.range u)`
+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
+  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
+  suffices x ∈ s by specialize hst x; simp_all
+  refine hsc.mem_of_tendsto hux <| eventually_of_forall fun k ↦ ?_
+  specialize hst (u k)
+  simp_all
+
+/-- A sequential space is compactly generated. -/
+lemma isCompact_of_seq [SequentialSpace X] : RestrictGenTopology {K : Set X | IsCompact K} :=
+  of_seq fun _u _x hux ↦ hux.isCompact_insert_range
+
+end RestrictGenTopology

Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

@@ -6,6 +6,7 @@ Authors: Anatole Dedecker
 import Mathlib.Topology.UniformSpace.UniformConvergence
 import Mathlib.Topology.UniformSpace.Pi
 import Mathlib.Topology.UniformSpace.Equiv
+import Mathlib.Topology.RestrictGenTopology
 
 #align_import topology.uniform_space.uniform_convergence_topology from "leanprover-community/mathlib"@"98e83c3d541c77cdb7da20d79611a780ff8e7d90"
 
@@ -1084,15 +1085,21 @@ 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_of_le [t : TopologicalSpace α]
-    (h : t ≤ ⨆ s ∈ 𝔖, .coinduced (Subtype.val : s → α) inferInstance) :
+theorem isClosed_setOf_continuous [TopologicalSpace α] (h : RestrictGenTopology 𝔖) :
     IsClosed {f : α →ᵤ[𝔖] β | Continuous (toFun 𝔖 f)} := by
-  refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ ?_
+  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
-  have hcont : ∀ s ∈ 𝔖, ContinuousOn f s := fun s hs ↦
-    (huf s hs).continuousOn <| hu fun _ ↦ Continuous.continuousOn
-  refine continuous_le_dom h ?_
-  simpa only [continuous_iSup_dom, continuous_coinduced_dom] using fun s hs ↦ (hcont s hs).restrict
+  exact (huf s hs).continuousOn <| hu fun _ ↦ Continuous.continuousOn
+
+/-- Suppose that the topology on `α` is defined by its restrictions to the sets of `𝔖`.
+
+Then the set of continuous functions is closed
+in the topology of uniform convergence on the sets of `𝔖`. -/
+@[deprecated isClosed_setOf_continuous (since := "2024-06-29")]
+theorem isClosed_setOf_continuous_of_le [t : TopologicalSpace α]
+    (h : t ≤ ⨆ s ∈ 𝔖, .coinduced (Subtype.val : s → α) inferInstance) :
+    IsClosed {f : α →ᵤ[𝔖] β | Continuous (toFun 𝔖 f)} :=
+  isClosed_setOf_continuous ⟨fun u hu ↦ h _ <| by simpa only [isOpen_iSup_iff, isOpen_coinduced]⟩
 
 variable (𝔖) in
 theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α)