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)
:
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)
:
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