Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: Small sets of games/surreals are bounded #10458

Closed
wants to merge 31 commits into from
Closed

[Merged by Bors] - feat: Small sets of games/surreals are bounded #10458

wants to merge 31 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Feb 12, 2024 •
edited by timotree3

Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in PGame.lean.

We don't port upper_bound_numeric (or lower_bound_numeric) because upper_bound was deleted following review feedback on the previous forward-porting PR #10566.

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Feb 12, 2024
@eric-wieser
Copy link
Member

I think we should regenerate that page one last time, if these really are the final forward ports

@YaelDillies
Copy link
Collaborator Author

That would be great but I don't know how to do that.

@urkud
Copy link
Member

urkud commented Feb 14, 2024

Could you please split it into smaller PRs, each for 1 topic?

@urkud urkud added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Feb 14, 2024
@urkud urkud self-assigned this Feb 14, 2024
@YaelDillies
Copy link
Collaborator Author

It's a bit of a pain to split, so I'll only do it if you have a specific thing you would like to see in another PR.

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Feb 14, 2024
YaelDillies and others added 2 commits February 14, 2024 16:09
@YaelDillies @urkud
golf
1f7f6a2 
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@YaelDillies
reuse variables
9501869
@timotree3 timotree3 added awaiting-review The author would like community review of the PR and removed delegated labels Mar 3, 2024
eric-wieser
eric-wieser approved these changes Mar 8, 2024
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

bors merge

Thanks!

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Mar 8, 2024
mathlib-bors bot pushed a commit that referenced this pull request Mar 8, 2024
@YaelDillies @urkud @timotree3
feat: Small sets of games/surreals are bounded (#10458)
776be0d 
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 8, 2024

Build failed:

@eric-wieser
Copy link
Member

bors r-

bors d+

Looks like an easy fix.

@mathlib-bors
Copy link

mathlib-bors bot commented Mar 8, 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.

@YaelDillies
Copy link
Collaborator Author

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 9, 2024
@YaelDillies @urkud @timotree3
feat: Small sets of games/surreals are bounded (#10458)
96ef680 
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 9, 2024

Build failed:

@YaelDillies
Copy link
Collaborator Author

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 9, 2024
@YaelDillies @urkud @timotree3
feat: Small sets of games/surreals are bounded (#10458)
d004cbb 
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 9, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Small sets of games/surreals are bounded [Merged by Bors] - feat: Small sets of games/surreals are bounded Mar 9, 2024
@mathlib-bors mathlib-bors bot closed this Mar 9, 2024
@mathlib-bors mathlib-bors bot deleted the forward_ports branch March 9, 2024 22:56
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@YaelDillies @urkud
@timotree3 @kbuzzard
feat: Small sets of games/surreals are bounded (#10458)
0e9d003 
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@YaelDillies @urkud
@timotree3 @dagurtomas
feat: Small sets of games/surreals are bounded (#10458)
2129ca0 
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
utensil pushed a commit that referenced this pull request Mar 26, 2024
@YaelDillies @urkud
@timotree3 @utensil
feat: Small sets of games/surreals are bounded (#10458)
9493f20 
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@YaelDillies @urkud
@timotree3 @Louddy
feat: Small sets of games/surreals are bounded (#10458)
b72118a 
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@YaelDillies @urkud
@timotree3 @uniwuni
feat: Small sets of games/surreals are bounded (#10458)
347c5b0 
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@YaelDillies @urkud
@timotree3 @callesonne
feat: Small sets of games/surreals are bounded (#10458)
e6c8970 
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
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

@timotree3 timotree3 timotree3 approved these changes

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees

@urkud urkud

@eric-wieser eric-wieser

Labels
delegated 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-logic Logic (model theory, set theory, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@YaelDillies @eric-wieser @urkud @timotree3 @Ruben-VandeVelde @leanprover-community-mathlib4-bot