Any T0 space embeds in a product of copies of the Sierpinski space.

We consider Prop with the Sierpinski topology. If X is a topological space, there is a continuous map productOfMemOpens from X to Opens X → Prop which is the product of the maps X → Prop given by x ↦ x ∈ u.

The map productOfMemOpens is always inducing. Whenever X is T0, productOfMemOpens is also injective and therefore an embedding.

theorem TopologicalSpace.eq_induced_by_maps_to_sierpinski (X : Type u_1) [t : TopologicalSpace X] : t = ⨅ (u : TopologicalSpace.Opens X), TopologicalSpace.induced (fun (x : X) => x ∈ u) sierpinskiSpace

def TopologicalSpace.productOfMemOpens (X : Type u_1) [TopologicalSpace X] : C(X, TopologicalSpace.Opens X → Prop)

The continuous map from X to the product of copies of the Sierpinski space, (one copy for each open subset u of X). The u coordinate of productOfMemOpens x is given by x ∈ u.

Equations

• TopologicalSpace.productOfMemOpens X = ContinuousMap.mk fun (x : X) (u : TopologicalSpace.Opens X) => x ∈ u

theorem TopologicalSpace.productOfMemOpens_inducing (X : Type u_1) [TopologicalSpace X] : Inducing ⇑(TopologicalSpace.productOfMemOpens X)

theorem TopologicalSpace.productOfMemOpens_injective (X : Type u_1) [TopologicalSpace X] [T0Space X] : Function.Injective ⇑(TopologicalSpace.productOfMemOpens X)

theorem TopologicalSpace.productOfMemOpens_embedding (X : Type u_1) [TopologicalSpace X] [T0Space X] : Embedding ⇑(TopologicalSpace.productOfMemOpens X)