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 : Opens X), induced (fun (x : X) => x ∈ u) sierpinskiSpace

def TopologicalSpace.productOfMemOpens (X : Type u_1) [TopologicalSpace X] : C(X, 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 = { toFun := fun (x : X) (u : TopologicalSpace.Opens X) => x ∈ u, continuous_toFun := ⋯ }

theorem TopologicalSpace.productOfMemOpens_isInducing (X : Type u_1) [TopologicalSpace X] : Topology.IsInducing ⇑(productOfMemOpens X)

@[deprecated TopologicalSpace.productOfMemOpens_isInducing (since := "2024-10-28")]

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

Alias of TopologicalSpace.productOfMemOpens_isInducing.

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

theorem TopologicalSpace.productOfMemOpens_isEmbedding (X : Type u_1) [TopologicalSpace X] [T0Space X] : Topology.IsEmbedding ⇑(productOfMemOpens X)

@[deprecated TopologicalSpace.productOfMemOpens_isEmbedding (since := "2024-10-26")]

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

Alias of TopologicalSpace.productOfMemOpens_isEmbedding.