Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-12 14:51 1e0761e5

View on Github →

feat(topology/maps): closed embeddings (#1013)

feat(topology/maps): closed embeddings
fix "is_open_map"

Estimated changes

Modified src/topology/maps.lean

added theorem closed_embedding.closed_iff_image_closed

added theorem closed_embedding.closed_iff_preimage_closed

added def closed_embedding

added theorem closed_embedding_compose

added theorem closed_embedding_id

added theorem closed_embedding_of_continuous_injective_closed

added theorem is_closed_map.of_inverse

added def is_closed_map