Commit 2020-05-31 01:56 297806e6

View on Github →

feat(topology/homeomorph): sum_prod_distrib (#2870) Also modify the inv_fun of equiv.sum_prod_distrib to have more useful definitional behavior. This also simplifies measurable_equiv.sum_prod_distrib.

Estimated changes

Modified src/data/equiv/basic.lean

Modified src/measure_theory/measurable_space.lean

Modified src/topology/constructions.lean

modified theorem continuous_inl

modified theorem continuous_inr

modified theorem embedding_inl

modified theorem embedding_inr

added theorem is_open_map_sum

added theorem is_open_sum_iff

added theorem open_embedding_inl

added theorem open_embedding_inr

Modified src/topology/homeomorph.lean

added def homeomorph.prod_sum_distrib

added def homeomorph.sum_congr

added def homeomorph.sum_prod_distrib