Skip to content

[Merged by Bors] - chore: Rename DenseEmbedding to IsDenseEmbedding#17247

Closed
YaelDillies wants to merge 7 commits intomasterfrom
rename_dense_embedding
Closed

[Merged by Bors] - chore: Rename DenseEmbedding to IsDenseEmbedding#17247
YaelDillies wants to merge 7 commits intomasterfrom
rename_dense_embedding

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Sep 29, 2024

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.

Open in Gitpod

@YaelDillies YaelDillies added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Sep 29, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 29, 2024 •
edited
Loading

PR summary 0135401b64

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Dense.isDenseEmbedding_val
+ IsDenseEmbedding
+ IsDenseEmbedding.mk'
+ UniformEmbedding.isDenseEmbedding
+ id
+ isDenseEmbedding_coe_real
+ isDenseEmbedding_pure
+ isDenseEmbedding_pureCauchy
++ isDenseEmbedding_coe
+++ isDenseEmbedding
+++--- denseEmbedding
++-- denseEmbedding_coe
- DenseEmbedding

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@YaelDillies YaelDillies mentioned this pull request Sep 29, 2024
Closed
11 tasks
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Sep 29, 2024

Can you add deprecations?

@YaelDillies YaelDillies force-pushed the rename_dense_embedding branch from 6e59ac5 to 9fa91c4 Compare September 30, 2024 09:11
sgouezel
sgouezel reviewed Sep 30, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 30, 2024

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Sep 30, 2024
@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Sep 30, 2024

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Sep 30, 2024
@YaelDillies
chore: Rename DenseEmbedding to IsDenseEmbedding (#17247)
2db234e 
`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.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: Rename DenseEmbedding to IsDenseEmbedding [Merged by Bors] - chore: Rename DenseEmbedding to IsDenseEmbedding Sep 30, 2024
@mathlib-bors mathlib-bors bot closed this Sep 30, 2024
@mathlib-bors mathlib-bors bot deleted the rename_dense_embedding branch September 30, 2024 14:37
chrisflav pushed a commit that referenced this pull request Oct 1, 2024
@YaelDillies @chrisflav
chore: Rename DenseEmbedding to IsDenseEmbedding (#17247)
b131a65 
`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.
fbarroero pushed a commit that referenced this pull request Oct 2, 2024
@YaelDillies @fbarroero
chore: Rename DenseEmbedding to IsDenseEmbedding (#17247)
55bd0f8 
`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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@YaelDillies @sgouezel