Mathlib v3 is deprecated. Go to Mathlib v4

Theorem homeomorph.coe_punit_prod

Modification history

2021-02-11 20:21

src/topology/homeomorph.lean

chore(topology/homeomorph): review, add `prod_punit`/`punit_prod` (#6180) …

Added homeomorph.coe_punit_prod View on Github →