Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-18 17:59 066d0535

View on Github →

chore(topology/maps): a few tweaks to open_embedding and closed embeddings (#1459)

chore(topology/maps): a few tweaks to open_embedding and closed embeddings aligning them with recent modification to embedding. From the perfectoid project.
chore(topology/maps): add missing empty line

Estimated changes

Modified src/topology/maps.lean

modified theorem closed_embedding.closed_iff_image_closed

modified theorem closed_embedding.closed_iff_preimage_closed

added theorem closed_embedding.continuous

modified theorem closed_embedding.is_closed_map

added structure closed_embedding

deleted def closed_embedding

modified theorem closed_embedding_of_continuous_injective_closed

modified theorem closed_embedding_of_embedding_closed

added theorem open_embedding.comp

added theorem open_embedding.continuous

added structure open_embedding

deleted def open_embedding

deleted theorem open_embedding_compose

added theorem subtype_val.closed_embedding

added theorem subtype_val.open_embedding