Skip to content

[Merged by Bors] - feat: port Topology.MetricSpace.Lipschitz#2634

Closed
urkud wants to merge 6 commits intomasterfrom
port/Topology.MetricSpace.Lipschitz
Closed

[Merged by Bors] - feat: port Topology.MetricSpace.Lipschitz#2634
urkud wants to merge 6 commits intomasterfrom
port/Topology.MetricSpace.Lipschitz

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Mar 4, 2023

Open in Gitpod

@urkud urkud force-pushed the port/Topology.MetricSpace.Lipschitz branch from 8bd4fdf to 05b019d Compare March 4, 2023 17:11
urkud
urkud commented Mar 4, 2023
View reviewed changes
Comment thread Mathlib/Topology/MetricSpace/Lipschitz.lean Outdated
@urkud urkud force-pushed the port/Topology.MetricSpace.Lipschitz branch from f922b0f to 7a24ca8 Compare March 5, 2023 07:52
@urkud urkud force-pushed the port/Topology.MetricSpace.Lipschitz branch from 7a24ca8 to 218873c Compare March 6, 2023 07:33
@urkud urkud added awaiting-review mathlib-port This is a port of a theory file from mathlib. labels Mar 6, 2023
jcommelin
jcommelin approved these changes Mar 6, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Mar 6, 2023

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

@jcommelin jcommelin added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 6, 2023
@kim-em kim-em added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Mar 6, 2023
@urkud
Copy link
Copy Markdown
Member Author

urkud commented Mar 6, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Mar 6, 2023
bors bot pushed a commit that referenced this pull request Mar 6, 2023
@urkud
feat: port Topology.MetricSpace.Lipschitz (#2634)
aeba075
@bors
Copy link
Copy Markdown

bors bot commented Mar 6, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Topology.MetricSpace.Lipschitz [Merged by Bors] - feat: port Topology.MetricSpace.Lipschitz Mar 6, 2023
@bors bors bot closed this Mar 6, 2023
@bors bors bot deleted the port/Topology.MetricSpace.Lipschitz branch March 6, 2023 09:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

Labels

awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@urkud @jcommelin @kim-em
⚡