Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-13 23:54 07ba43ee

View on Github →

feat(topology/constructions): topology of sum types (#1016)

Estimated changes

Modified src/data/sigma/basic.lean

added theorem injective_sigma_map

added theorem injective_sigma_mk

Modified src/topology/constructions.lean

added theorem closed_embedding_sigma_mk

added theorem continuous_sigma

added theorem continuous_sigma_map

added theorem continuous_sigma_mk

added theorem embedding_sigma_map

added theorem embedding_sigma_mk

added theorem is_closed_map_sigma_mk

added theorem is_closed_sigma_iff

added theorem is_closed_sigma_mk

added theorem is_open_map_sigma_mk

added theorem is_open_range_sigma_mk

added theorem is_open_sigma_iff

Modified src/topology/maps.lean

deleted theorem continuous_Prop

deleted theorem is_open_singleton_true

Modified src/topology/order.lean

added theorem continuous_Prop

added theorem is_closed_infi_iff

added theorem is_open_infi_iff

added theorem is_open_singleton_true