Commit 2024-10-20 13:29 0dedd92e

View on Github →

chore: Rename ClosedEmbedding to IsClosedEmbedding (#17937) 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 ClosedEmbedding is)
  2. namespacing it inside Topology Zulip. See #15993 for context.

Estimated changes