Skip to content

[Merged by Bors] - chore: Rename DenseInducing to IsDenseInducing#17208

Closed
YaelDillies wants to merge 3 commits intomasterfrom
rename_dense_inducing
Closed

[Merged by Bors] - chore: Rename DenseInducing to IsDenseInducing#17208
YaelDillies wants to merge 3 commits intomasterfrom
rename_dense_inducing

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Sep 28, 2024 •
edited
Loading

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 DenseInducing is)
  2. namespacing it inside Topology

Zulip. See #15993 for context.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

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

PR summary 219c65002d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Filter.HasBasis.hasBasis_of_isDenseInducing
+ IsDenseInducing
+ IsDenseInducing.extendRingHom
+ UniformInducing.isDenseInducing
+ isDenseInducing_coe
+ isDenseInducing_pure
+ isDenseInducing_pureCauchy
+ isDenseInducing_toCompl
++ isDenseInducing
- DenseInducing
- DenseInducing.extendRingHom
- Filter.HasBasis.hasBasis_of_denseInducing
- UniformInducing.denseInducing
- denseInducing_coe
- denseInducing_pure
- denseInducing_pureCauchy
- denseInducing_toCompl
-- denseInducing

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 added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Sep 28, 2024
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Sep 28, 2024

Can you describe the motivation for this rename?

@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Sep 28, 2024

Function.Embedding is a type while Embedding is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence I am suggesting

  1. To rename Embedding to IsEmbedding and similarly for neighborhing declarations (which DenseInducing is)
  2. To namespace it inside Topology

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Sep 28, 2024 •
edited
Loading

Please explain that in the PR description!

It sounds to me like it would make more sense to rename Embedding first, but I guess it doesn't really matter if it all happens soon anyway.

In isolation, Inducing feels different to Embedding since only the latter is a noun.

@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Sep 28, 2024

Embedding is the declaration with the biggest fallout, so my plan is to do it last.

In isolation, Inducing feels different to Embedding since only the latter is a noun.

Maybe, but I think Inducing/IsEmbedding is strictly worse than IsInducing/IsEmbedding. Also note that mathlib docstrings have started using "inducing" as a noun!

@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Sep 28, 2024 •
edited
Loading

Please update the PR description per Eric's comment, as we want this in the git history.

Also, It doesn't look like you namespaced IsDenseInducing. Or did I miss it (I only looked on GitHub)?

@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Sep 28, 2024

As clarified on Zulip, namespacing will be done later, all declarations at once

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Sep 28, 2024

Also note that mathlib docstrings have started using "inducing" as a noun!

Can you give an example, and maybe raise this on zulip?

@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Sep 28, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 28, 2024
mathlib-bors bot pushed a commit that referenced this pull request Sep 29, 2024
@YaelDillies
chore: Rename DenseInducing to IsDenseInducing (#17208)
0668f23 
`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 `DenseInducing` 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 29, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: Rename DenseInducing to IsDenseInducing [Merged by Bors] - chore: Rename DenseInducing to IsDenseInducing Sep 29, 2024
@mathlib-bors mathlib-bors bot closed this Sep 29, 2024
@mathlib-bors mathlib-bors bot deleted the rename_dense_inducing branch September 29, 2024 00:39
@YaelDillies YaelDillies mentioned this pull request Sep 29, 2024
Closed
11 tasks
fbarroero pushed a commit that referenced this pull request Oct 2, 2024
@YaelDillies @fbarroero
chore: Rename DenseInducing to IsDenseInducing (#17208)
5fa6345 
`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 `DenseInducing` 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

No reviews

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. 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.

3 participants

@YaelDillies @eric-wieser @j-loreaux