Commit 2024-10-03 20:47 3ca1060d

View on Github →

chore: Rename UniformEmbedding to IsUniformEmbedding (#17295) 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 DenseEmbedding is)
  2. namespacing it inside Topology Zulip. See #15993 for context.

Estimated changes

deleted theorem Equiv.uniformEmbedding
added structure IsUniformEmbedding
deleted theorem UniformEmbedding.comp
deleted theorem UniformEmbedding.prod
deleted structure UniformEmbedding
modified theorem completeSpace_congr
added theorem isUniformEmbedding_inl
added theorem isUniformEmbedding_inr
deleted theorem uniformEmbedding_comap
deleted theorem uniformEmbedding_iff'
deleted theorem uniformEmbedding_inl
deleted theorem uniformEmbedding_inr