[Merged by Bors] - chore: Rename UniformEmbedding to IsUniformEmbedding#17295
[Merged by Bors] - chore: Rename UniformEmbedding to IsUniformEmbedding#17295YaelDillies wants to merge 10 commits intomasterfrom
UniformEmbedding to IsUniformEmbedding#17295Conversation
PR summary 633bfedd11Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
`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](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rename.20.60Inducing.60.20and.20.60Embedding.60.3F). See #15993 for context.
ac10a4f to
fa6d5d4
Compare
|
Please ensure your PR titles follow the mathlib convention: https://leanprover-community.github.io/contribute/commit.html |
j-loreaux
left a comment
There was a problem hiding this comment.
Unless I missed them, there are a few deprecations missing.
bors d+
| injective. If `α` is a separated space, then the latter assumption follows from the former. -/ | ||
| @[mk_iff] | ||
| structure UniformEmbedding (f : α → β) extends UniformInducing f : Prop where | ||
| structure IsUniformEmbedding (f : α → β) extends UniformInducing f : Prop where |
There was a problem hiding this comment.
@adomani, all the deprecations were generated using your script, so you want to see which were missing to fix the script. Looks like it missed structure and abbrev
There was a problem hiding this comment.
I think that the deprecation script was a precursor to the decl_diff script and is missing all the future improvements that were added to decl_diff.
I'll see if I get a chance to modify the decl_diff script, or at least try to merge it into the deprecation one, though the term has started and I have less time available now.
There was a problem hiding this comment.
@YaelDillies, I adapted the script and ran it from your first commit. Besides what I think were the modifications that you also had there, it added a few more, such as
@@ -104,6 +104,9 @@ abbrev IsUniformEmbedding.comapMetricSpace {α β} [UniformSpace α] [m : Metric
(h : IsUniformEmbedding f) : MetricSpace α :=
.replaceUniformity (.induced f h.inj m) h.comap_uniformity.symm
+@[deprecated (since := "2024-10-04")]
+alias UniformEmbedding.comapMetricSpace := IsUniformEmbedding.comapMetricSpace
+
@@ -222,6 +222,9 @@ noncomputable def ofIsUniformEmbedding (f : α → β) (hf : IsUniformEmbedding
exact uniformContinuous_subtype_val
toEquiv := Equiv.ofInjective f hf.inj
+@[deprecated (since := "2024-10-04")]
+alias ofUniformEmbedding := ofIsUniformEmbedding
+
@@ -134,12 +134,15 @@ structure IsUniformEmbedding (f : α → β) extends UniformInducing f : Prop wh
/-- A uniform embedding is injective. -/
inj : Function.Injective f
+@[deprecated (since := "2024-10-04")]
+alias UniformEmbedding := IsUniformEmbedding
+
#### not sure about this one in `Mathlib/Topology/UniformSpace/UniformEmbedding.lean` ~270
+@[deprecated (since := "2024-10-04")]
+alias UniformEmbedding.denseEmbedding := IsUniformEmbedding.denseEmbedding
+I imagine that these are the ones that were later flagged by Jireh. The last one seems strange. There were others as well, but they looked more like later changes to master.
There was a problem hiding this comment.
Interesting! Please post the updated script on Zulip
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
`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](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rename.20.60Inducing.60.20and.20.60Embedding.60.3F). See #15993 for context.
|
Pull request successfully merged into master. Build succeeded: |
UniformEmbedding to IsUniformEmbeddingUniformEmbedding to IsUniformEmbedding
Function.Embeddingis a type whileEmbeddingis a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towardsEmbeddingtoIsEmbeddingand similarly for neighborhing declarations (whichDenseEmbeddingis)TopologyZulip. See #15993 for context.