Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_space.product_of_mem_opens_injective

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.product_of_mem_opens_injectiveView on Github →