[Merged by Bors] - refactor(set_theory/game/*): Fix bad notation < on (pre-)games
#13963
Conversation
vihdzp
changed the title
<< on (pre-)games
|
Seems you didn't exhibit a |
|
I did make an |
|
Note: I moved a lot of theorems around on |
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Scott Morrison <scott@tqft.net>
|
Great, if CI passes you can ask bors to merge it. bors d+ |
|
✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
There was a problem hiding this comment.
The PR looks good in general; the added lemmas all seem to be an integral part of the refactoring. However it's a big diff so I have quite a few comments.
There are several reordering of code that I don't quite understand (doesn't seem to golf anything, so it seems to me that they make the diff unnecessarily large.
I believe I marked all lemmas that are removed instead of replaced by the corresponding ones under the new notation. I think it's a good idea to keep them in general.
|
bors r+ |
) Our current definition for `<` on pre-games is, in the wider mathematical literature, referred to as `⧏` (less or fuzzy to). Conversely, what's usually referred to by `<` coincides with the relation we get from `preorder pgame` (which the current API avoids using at all). We rename `<` to `⧏`, and add the basic API for both the new `<` and `⧏` relations. This allows us to define new instances on `pgame` and `game` that we couldn't before. We also take the opportunity to add some basic API on the fuzzy relation `∥`. See the [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Surreal.20numbers/near/281094687).
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
< on (pre-)games< on (pre-)games
Our current definition for
<on pre-games is, in the wider mathematical literature, referred to as⧏(less or fuzzy to). Conversely, what's usually referred to by<coincides with the relation we get frompreorder pgame(which the current API avoids using at all).We rename
<to⧏, and add the basic API for both the new<and⧏relations. This allows us to define new instances onpgameandgamethat we couldn't before. We also take the opportunity to add some basic API on the fuzzy relation∥.See the Zulip discussion.
Note that the file
winner.leannow consists entirely of one-line statements. I'll propose its deletion in an upcoming PR.