Open or closed subsets that are also X-generated spaces

Let X : ι → Type* be a family of topological spaces. If all the opens (resp. closed) subsets of the X i are X-generated, then any open (resp. closed) subset of an X-generated space is X-generated.

theorem IsOpen.isGeneratedBy {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {Y : Type u_3} [TopologicalSpace Y] [∀ (i : ι) (U : TopologicalSpace.Opens (X i)), Topology.IsGeneratedBy X ↥U] [Topology.IsGeneratedBy X Y] {U : Set Y} (hU : IsOpen U) : Topology.IsGeneratedBy X ↑U

theorem Topology.IsOpenEmbedding.isGeneratedBy {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {Y : Type u_3} [TopologicalSpace Y] [∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U] [IsGeneratedBy X Y] {F : Type u_4} [TopologicalSpace F] {f : F → Y} (hf : IsOpenEmbedding f) : IsGeneratedBy X F

theorem IsClosed.isGeneratedBy {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {Y : Type u_3} [TopologicalSpace Y] [∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), Topology.IsGeneratedBy X ↥F] [Topology.IsGeneratedBy X Y] {F : Set Y} (hF : IsClosed F) : Topology.IsGeneratedBy X ↑F

theorem Topology.IsClosedEmbedding.isGeneratedBy {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {Y : Type u_3} [TopologicalSpace Y] [∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F] [IsGeneratedBy X Y] {U : Type u_4} [TopologicalSpace U] {f : U → Y} (hf : IsClosedEmbedding f) : IsGeneratedBy X U