Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_space.eq_induced_by_maps_to_sierpinski

Modification history

2022-07-08 02:55

src/topology/continuous_function/t0_sierpinski.lean

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

Added topological_space.eq_induced_by_maps_to_sierpinski View on Github →