Commit 2024-10-18 21:29 de5d061f

View on Github →

chore: Rename OpenEmbedding to IsOpenEmbedding (#17898) Function.Embedding is a type while Embedding is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards

  1. renaming Embedding to IsEmbedding and similarly for neighborhing declarations (which OpenEmbedding is)
  2. namespacing it inside Topology Zulip. See #15993 for context.

Estimated changes

deleted theorem OpenEmbedding.continuous
deleted theorem OpenEmbedding.isOpenMap
deleted theorem OpenEmbedding.map_nhds_eq
deleted theorem OpenEmbedding.of_comp
deleted theorem OpenEmbedding.of_comp_iff
deleted theorem OpenEmbedding.of_isEmpty
added theorem isOpenEmbedding_id
deleted theorem openEmbedding_id