mathlib3
834488ee - feat(topology/maps): more `iff` lemmas (#15165)

Commit
3 years ago
feat(topology/maps): more `iff` lemmas (#15165) * add `inducing_iff` and `inducing_iff_nhds`; * add `embedding_iff`; * add `open_embedding_iff_embedding_open` and `open_embedding_iff_continuous_injective_open`; * add `open_embedding.is_open_map_iff`; * reorder `open_embedding_iff_open_embedding_compose` and `open_embedding_of_open_embedding_compose`, golf.
Author
Parents
Loading