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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

source

theorem topological_space.eq_induced_by_maps_to_sierpinski (X : Type u_1) [t : topological_space X] :

t = ⨅ (u : topological_space.opens X), topological_space.induced (λ (_x : X), _x ∈ u) sierpinski_space

source

def topological_space.product_of_mem_opens (X : Type u_1) [topological_space X] :

C(X, topological_space.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 product_of_mem_opens x is given by x ∈ u.

Equations

topological_space.product_of_mem_opens X = {to_fun := λ (x : X) (u : topological_space.opens X), x ∈ u, continuous_to_fun := _}

source

theorem topological_space.product_of_mem_opens_inducing (X : Type u_1) [topological_space X] :

inducing ⇑(topological_space.product_of_mem_opens X)

source

theorem topological_space.product_of_mem_opens_injective (X : Type u_1) [topological_space X] [t0_space X] :

function.injective ⇑(topological_space.product_of_mem_opens X)

source

theorem topological_space.product_of_mem_opens_embedding (X : Type u_1) [topological_space X] [t0_space X] :

embedding ⇑(topological_space.product_of_mem_opens X)