[Merged by Bors] - chore: Rename UniformInducing to IsUniformInducing#17398
[Merged by Bors] - chore: Rename UniformInducing to IsUniformInducing#17398YaelDillies wants to merge 3 commits intomasterfrom
UniformInducing to IsUniformInducing#17398Conversation
PR summary 4f895c9eb6Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
b8da38d to
c8245d2
Compare
`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 `UniformInducing` 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.
b7d5f40 to
fe5b5c8
Compare
| separation : T0Space space | ||
| /-- The map into the completion is uniform-inducing. -/ | ||
| uniformInducing : UniformInducing coe | ||
| isUniformInducing : IsUniformInducing coe |
There was a problem hiding this comment.
I realize this is a structure field. Do we provide deprecations for these? It seems less necessary because Lean should normally be able to tell the user what the problem is.
There was a problem hiding this comment.
Doesn't cost much to add it, so I've added it.
cc @adomani if you want to modify the script to account for structure field renames
|
✌️ 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 `UniformInducing` 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: |
UniformInducing to IsUniformInducingUniformInducing to IsUniformInducing
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 (whichUniformInducingis)TopologyZulip. See #15993 for context.