Skip to content

[Merged by Bors] - chore: forward-port leanprover-community/mathlib#19028#8083

Closed
eric-wieser wants to merge 3 commits intomasterfrom
forward-port-19028
Closed

[Merged by Bors] - chore: forward-port leanprover-community/mathlib#19028#8083
eric-wieser wants to merge 3 commits intomasterfrom
forward-port-19028

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Nov 1, 2023

This was "feat(topology/metric_space): diameter of pointwise zero and addition"

Open in Gitpod

@eric-wieser
chore: forward-port leanprover-community/mathlib3#19028
033f394 
This was "feat(topology/metric_space): diameter of pointwise zero and addition"
@eric-wieser eric-wieser added mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged t-analysis Analysis (normed *, calculus) awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Nov 1, 2023
eric-wieser
eric-wieser commented Nov 1, 2023
View reviewed changes
Mathlib/Topology/Bornology/Basic.lean
Copy link
Copy Markdown
Member Author

@eric-wieser eric-wieser Nov 1, 2023 •
edited
Loading

Choose a reason for hiding this comment

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

This file has no SHA change since the result was moved from another file.

YaelDillies
YaelDillies approved these changes Nov 1, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Thanks. This is an accurate forward-port!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 1, 2023

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

@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Nov 1, 2023

Thanks!

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Nov 1, 2023

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

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Nov 1, 2023
@eric-wieser
Copy link
Copy Markdown
Member Author

eric-wieser commented Nov 1, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 1, 2023
bors bot pushed a commit that referenced this pull request Nov 1, 2023
@eric-wieser
chore: forward-port leanprover-community/mathlib3#19028 (#8083)
5a2b014 
This was "feat(topology/metric_space): diameter of pointwise zero and addition"
@bors
Copy link
Copy Markdown

bors bot commented Nov 1, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore: forward-port leanprover-community/mathlib#19028 [Merged by Bors] - chore: forward-port leanprover-community/mathlib#19028 Nov 1, 2023
@bors bors bot closed this Nov 1, 2023
@bors bors bot deleted the forward-port-19028 branch November 1, 2023 16:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@eric-wieser @riccardobrasca @YaelDillies