Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-07 05:32 10cb0d12

View on Github →

feat(topology/constructions): distributivity of products over sums (#1059)

feat(topology/constructions): distributivity of products over sums
Update src/topology/maps.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Reverse direction of sigma_prod_distrib

Estimated changes

Modified src/data/equiv/basic.lean

added def equiv.sigma_prod_distrib

Modified src/data/set/lattice.lean

added theorem set.Union_image_preimage_sigma_mk_eq_self

Modified src/topology/constructions.lean

added def homeomorph.homeomorph_of_continuous_open

added def homeomorph.sigma_prod_distrib

added theorem is_open_map_sigma

added theorem open_embedding_sigma_mk

Modified src/topology/maps.lean

added theorem closed_embedding.is_closed_map

added theorem closed_embedding_of_embedding_closed

added theorem open_embedding.is_open_map

added theorem open_embedding.open_iff_image_open

added theorem open_embedding.open_iff_preimage_open

added def open_embedding

added theorem open_embedding_compose

added theorem open_embedding_id

added theorem open_embedding_of_continuous_injective_open

added theorem open_embedding_of_embedding_open