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 Mathlib/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}.

theorem Topology.RestrictGenTopology.isOpen_iff {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} {t : Set X} (hS : Topology.RestrictGenTopology S) : IsOpen t ↔ ∀ s ∈ S, IsOpen (Subtype.val ⁻¹' t)

theorem Topology.RestrictGenTopology.isClosed_iff {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} {t : Set X} (hS : Topology.RestrictGenTopology S) : IsClosed t ↔ ∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)

theorem Topology.RestrictGenTopology.continuous_iff {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} {Y : Type u_2} [TopologicalSpace Y] {f : X → Y} (hS : Topology.RestrictGenTopology S) : Continuous f ↔ ∀ s ∈ S, ContinuousOn f s

theorem Topology.RestrictGenTopology.of_continuous_prop {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} (h : ∀ (f : X → Prop), (∀ s ∈ S, ContinuousOn f s) → Continuous f) : Topology.RestrictGenTopology S

theorem Topology.RestrictGenTopology.of_isClosed {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} (h : ∀ (t : Set X), (∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)) → IsClosed t) : Topology.RestrictGenTopology S

theorem Topology.RestrictGenTopology.enlarge {X : Type u_1} [TopologicalSpace X] {S T : Set (Set X)} (hS : Topology.RestrictGenTopology S) (hT : ∀ s ∈ S, ∃ t ∈ T, s ⊆ t) : Topology.RestrictGenTopology T

theorem Topology.RestrictGenTopology.mono {X : Type u_1} [TopologicalSpace X] {S T : Set (Set X)} (hS : Topology.RestrictGenTopology S) (hT : S ⊆ T) : Topology.RestrictGenTopology T

theorem Topology.RestrictGenTopology.of_seq {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} [SequentialSpace X] (h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Filter.Tendsto u Filter.atTop (nhds x) → insert x (Set.range u) ∈ S) : Topology.RestrictGenTopology S

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.

theorem Topology.RestrictGenTopology.isCompact_of_seq {X : Type u_1} [TopologicalSpace X] [SequentialSpace X] : Topology.RestrictGenTopology {K : Set X | IsCompact K}

A sequential space is compactly generated.

theorem Topology.RestrictGenTopology.of_nhds {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} (h : ∀ (x : X), ∃ s ∈ S, s ∈ nhds x) : Topology.RestrictGenTopology S

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.

theorem Topology.RestrictGenTopology.isCompact_of_weaklyLocallyCompact {X : Type u_1} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] : Topology.RestrictGenTopology {K : Set X | IsCompact K}

A weakly locally compact space is compactly generated.