Commit 2021-05-08 08:13 4a8a5950

View on Github →

feat(topology/subset_properties, homeomorph): lemmata about embeddings (#7431) Two lemmata: (i) embedding to homeomorphism (ii) a closed embedding is proper Coauthored with @hrmacbeth

Estimated changes

Modified src/data/equiv/basic.lean

added theorem equiv.self_comp_of_injective_symm

Modified src/topology/homeomorph.lean

Modified src/topology/subset_properties.lean

added theorem closed_embedding.tendsto_cocompact