mathlib

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

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 Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com>