Commit 2022-07-08 02:55 70a27086

View on Github →

feat(topology/continuous_function): Any T0 space embeds in a product of copies of the Sierpinski space (#14036) Any T0 space embeds in a product of copies of the Sierpinski space

Estimated changes

Created src/topology/continuous_function/t0_sierpinski.lean

added theorem topological_space.eq_induced_by_maps_to_sierpinski

added def topological_space.product_of_mem_opens

added theorem topological_space.product_of_mem_opens_embedding

added theorem topological_space.product_of_mem_opens_inducing

added theorem topological_space.product_of_mem_opens_injective

Modified src/topology/sets/opens.lean

added theorem topological_space.opens.mem_mk