Skip to content

[Merged by Bors] - chore: Namespace UniformSpace.ball API#16113

Closed
YaelDillies wants to merge 3 commits intomasterfrom
namespace_ball_mono
Closed

[Merged by Bors] - chore: Namespace UniformSpace.ball API#16113
YaelDillies wants to merge 3 commits intomasterfrom
namespace_ball_mono

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Aug 24, 2024

All these lemmas have pretty generic names

Open in Gitpod

@YaelDillies
chore: Namespace UniformSpace.ball API
29ab1c8 
All these lemmas have pretty generic names
@YaelDillies YaelDillies added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Aug 24, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 24, 2024 •
edited
Loading

PR summary ad451cee38

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ ball
+ isClosed_ball
+ isOpen_ball
+ mem_ball_self
- UniformSpace.ball
- UniformSpace.isClosed_ball
- UniformSpace.isOpen_ball
- UniformSpace.mem_ball_self

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.

grunweg
grunweg reviewed Aug 24, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

ball is used in many contexts, and this one clashes with Metric.ball --- seems reasonable to namespaces it.
maintainer merge

@grunweg grunweg changed the title chore: Namespace UniformSpace.ball API chore: namespace UniformSpace.ball API Aug 24, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 24, 2024

🚀 Pull request has been placed on the maintainer queue by grunweg.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 24, 2024
@YaelDillies YaelDillies changed the title chore: namespace UniformSpace.ball API chore: Namespace UniformSpace.ball API Aug 24, 2024
urkud
urkud reviewed Aug 24, 2024
View reviewed changes
@urkud urkud added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 24, 2024
@urkud
Copy link
Copy Markdown
Member

urkud commented Aug 24, 2024

Also, could you please add deprecated aliases?

@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Aug 25, 2024

Actually I don't think I should add deprecated aliases as they would conflict with the namespaced lemmas, forbidding everyone to open UniformSpace

@YaelDillies YaelDillies removed awaiting-author A reviewer has asked the author a question or requested changes. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 25, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 30, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 30, 2024
@urkud
Copy link
Copy Markdown
Member

urkud commented Aug 31, 2024

Thanks! 🎉
bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 31, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 31, 2024
@YaelDillies
chore: Namespace UniformSpace.ball API (#16113)
bf4eb84 
All these lemmas have pretty generic names
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 31, 2024

This PR was included in a batch that was canceled, it will be automatically retried

mathlib-bors bot pushed a commit that referenced this pull request Aug 31, 2024
@YaelDillies
chore: Namespace UniformSpace.ball API (#16113)
b5690db 
All these lemmas have pretty generic names
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 31, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: Namespace UniformSpace.ball API [Merged by Bors] - chore: Namespace UniformSpace.ball API Aug 31, 2024
@mathlib-bors mathlib-bors bot closed this Aug 31, 2024
@mathlib-bors mathlib-bors bot deleted the namespace_ball_mono branch August 31, 2024 14:49
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@YaelDillies @bjoernkjoshanssen
chore: Namespace UniformSpace.ball API (#16113)
e3b546f 
All these lemmas have pretty generic names
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@YaelDillies @bjoernkjoshanssen
chore: Namespace UniformSpace.ball API (#16113)
ba8fe04 
All these lemmas have pretty generic names
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@YaelDillies @bjoernkjoshanssen
chore: Namespace UniformSpace.ball API (#16113)
12818e6 
All these lemmas have pretty generic names
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@urkud urkud urkud left review comments

@grunweg grunweg grunweg left review comments

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.

4 participants

@YaelDillies @urkud @grunweg @leanprover-community-bot-assistant