Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded#15260

Closed
vihdzp wants to merge 3 commits intomasterfrom
bdd_of_small_pgame
Closed

[Merged by Bors] - feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded#15260
vihdzp wants to merge 3 commits intomasterfrom
bdd_of_small_pgame

Conversation

@vihdzp
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp commented Jul 11, 2022

Open in Gitpod

@vihdzp vihdzp added the awaiting-review The author would like community review of the PR label Jul 11, 2022
kim-em
kim-em reviewed Nov 10, 2022
View reviewed changes
@kim-em kim-em 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 Nov 10, 2022
@vihdzp vihdzp added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 30, 2023
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Mar 30, 2023
@eric-wieser eric-wieser added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 15, 2023
@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented Jul 28, 2023

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jul 28, 2023
bors bot pushed a commit that referenced this pull request Jul 28, 2023
@vihdzp
feat(set_theory/game/pgame): small sets of pre-games / games / surrea…
8900d54 
…ls are bounded (#15260)
@bors
Copy link
Copy Markdown

bors bot commented Jul 28, 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 feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded [Merged by Bors] - feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded Jul 28, 2023
@bors bors bot closed this Jul 28, 2023
@bors bors bot deleted the bdd_of_small_pgame branch July 28, 2023 12:00
@YaelDillies YaelDillies mentioned this pull request Feb 14, 2024
Closed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 28, 2024
@YaelDillies
feat(SetTheory): Upper bound for games (#10566)
dba7545 
Partially forward-port leanprover-community/mathlib3#15260
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 28, 2024
@YaelDillies
feat(SetTheory): Upper bound for games (#10566)
74460c6 
Partially forward-port leanprover-community/mathlib3#15260
riccardobrasca pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 1, 2024
@YaelDillies @riccardobrasca
feat(SetTheory): Upper bound for games (#10566)
9647354 
Partially forward-port leanprover-community/mathlib3#15260
@YaelDillies YaelDillies mentioned this pull request Mar 2, 2024
Closed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 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/mathlib3#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 bot pushed a commit to leanprover-community/mathlib4 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/mathlib3#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 bot pushed a commit to leanprover-community/mathlib4 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/mathlib3#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>
kbuzzard pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 12, 2024
@YaelDillies @kbuzzard
feat(SetTheory): Upper bound for games (#10566)
7ba4b50 
Partially forward-port leanprover-community/mathlib3#15260
kbuzzard pushed a commit to leanprover-community/mathlib4 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/mathlib3#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 to leanprover-community/mathlib4 that referenced this pull request Mar 22, 2024
@YaelDillies @dagurtomas
feat(SetTheory): Upper bound for games (#10566)
999047c 
Partially forward-port leanprover-community/mathlib3#15260
dagurtomas pushed a commit to leanprover-community/mathlib4 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/mathlib3#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 to leanprover-community/mathlib4 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/mathlib3#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>
xgenereux pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 15, 2024
@YaelDillies @xgenereux
feat(SetTheory): Upper bound for games (#10566)
cf9b442 
Partially forward-port leanprover-community/mathlib3#15260
xgenereux pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 15, 2024
@YaelDillies @urkud
@timotree3 @xgenereux
feat: Small sets of games/surreals are bounded (#10458)
b72118a 
Finish forwarding porting leanprover-community/mathlib3#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 to leanprover-community/mathlib4 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/mathlib3#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 to leanprover-community/mathlib4 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/mathlib3#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>
chenjulang added a commit to chenjulang/mathlib that referenced this pull request May 11, 2024
@chenjulang
Merge commit '65a1391a0106c9204fe45bc73a039f056558cb83'
08049e0 
* commit '65a1391a0106c9204fe45bc73a039f056558cb83': (12443 commits)
  feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (leanprover-community#18087)
  feat(combinatorics/simple_graph): More clique lemmas (leanprover-community#19203)
  feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (leanprover-community#16976)
  move old README.md to OLD_README.md
  doc: Add a warning mentioning Lean 4 to the readme (leanprover-community#19243)
  feat(topology/metric_space): diameter of pointwise zero and addition (leanprover-community#19028)
  feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (leanprover-community#18629)
  feat(probability/independence): Independence of singletons (leanprover-community#18506)
  feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (leanprover-community#18612)
  feat(data/finset/lattice): `sup'`/`inf'` lemmas (leanprover-community#18989)
  chore(order/liminf_limsup): Generalise and move lemmas (leanprover-community#18628)
  feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for abelian categories (leanprover-community#17926)
  feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (leanprover-community#11352)
  feat(analysis/convex/proj_Icc): Extending convex functions (leanprover-community#18797)
  feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (leanprover-community#17925)
  feat(measure_theory/measure/haar_quotient): the Unfolding Trick (leanprover-community#18863)
  feat(linear_algebra/orientation): add `orientation.reindex` (leanprover-community#19236)
  feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths (leanprover-community#17828)
  feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (leanprover-community#15260)
  feat(tactic/positivity): Extension for `ite` (leanprover-community#17650)
  ...

# Conflicts:
#	README.md
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

1 more reviewer

@kim-em kim-em kim-em left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@digama0 digama0

Labels

not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@vihdzp @kim-em @eric-wieser @digama0