Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-12 21:43 834488ee

View on Github →

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.

Estimated changes

modified structure embedding
added theorem inducing_iff_nhds
added theorem open_embedding.of_comp