Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-11 20:21 cee5ddf3

View on Github →

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

use to_equiv := e instead of .. e to have definitional equality h.to_equiv = e;
add some @[simp] lemmas;
add homeomorph.prod_punit and homeomorph.punit_prod;
generalize unit.topological_space to punit.topological_space.

Estimated changes

Modified src/topology/homeomorph.lean

added theorem homeomorph.coe_prod_comm

added theorem homeomorph.coe_prod_congr

added theorem homeomorph.coe_prod_punit

added theorem homeomorph.coe_punit_prod

added theorem homeomorph.coe_refl

added theorem homeomorph.prod_comm_symm

added theorem homeomorph.prod_congr_symm

added def homeomorph.prod_punit

added def homeomorph.punit_prod

added theorem homeomorph.refl_symm

Modified src/topology/order.lean

Modified src/topology/topological_fiber_bundle.lean