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 IsCoherentWith in Mathlib/Topology/Defs/Induced.lean), and provide the others as corollaries.

Main results

• 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 IsCoherentWith S;

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

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

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

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

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

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

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

theorem Topology.IsCoherentWith.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) : IsCoherentWith 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.IsCoherentWith.of_nhds {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} (h : ∀ (x : X), ∃ s ∈ S, s ∈ nhds x) : IsCoherentWith 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.