Surreals 2 #4143
Merged
Surreals 2 #4143
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
icecream17
reviewed
Aug 19, 2024
changes-set.txt
Outdated
| @@ -99,6 +99,7 @@ make a github issue.) | |||
|
|
|||
| DONE: | |||
| Date Old New Notes | |||
| 19-Aug-24 rabeqdca [same] moved from SN's mathbox to main set.mm | |||
icecream17
reviewed
Aug 19, 2024
set.mm
Outdated
Comment on lines
530421
to
530445
| ${ | ||
| $d A x y $. | ||
| $( The left options of a surreal are less than that surreal. (Contributed | ||
| by Scott Fenton, 6-Aug-2024.) $) | ||
| llt $p |- ( A e. No -> ( _L ` A ) <<s { A } ) $= | ||
| ( vx vy csur wcel cleft cfv wss csn cv cslt wbr wral csslt leftf ffvelrni | ||
| cpw elpwid wa cvv snssi cbday cold crab leftval eleq2d breq1 elrab syl6bb | ||
| simplbda breq2 ralsng adantr mpbird ralrimiva w3a fvex snex pm3.2i brsslt | ||
| wb mpbiran syl3anbrc ) ADEZAFGZDHZAIZDHZBJZCJZKLZCVGMZBVEMZVEVGNLZVDVEDDD | ||
| QAFOPRADUAVDVLBVEVDVIVEEZSVLVIAKLZVDVOVIAUBGUCGZEZVPVDVOVIVJAKLZCVQUDZEVR | ||
| VPSVDVEVTVICAUEUFVSVPCVIVQVJVIAKUGUHUIUJVDVLVPVAVOVKVPCADVJAVIKUKULUMUNUO | ||
| VNVETEZVGTEZSVFVHVMUPWAWBAFUQAURUSBCVEVGUTVBVC $. | ||
|
|
||
| $( The right options of a surreal are greater than that surreal. | ||
| (Contributed by Scott Fenton, 6-Aug-2024.) $) | ||
| rgt $p |- ( A e. No -> { A } <<s ( _R ` A ) ) $= | ||
| ( vx vy csur wcel csn wss cright cfv cslt wbr wral csslt snssi cpw rightf | ||
| cv ffvelrni wa cvv elpwid cbday cold crab eleq2d breq2 elrab syl6bb simpr | ||
| rightval syl6bi ralrimiv wceq breq1 ralbidv ralsng mpbird w3a snex pm3.2i | ||
| fvex brsslt mpbiran syl3anbrc ) ADEZAFZDGZAHIZDGZBQZCQZJKZCVHLZBVFLZVFVHM | ||
| KZADNVEVHDDDOAHPRUAVEVNAVKJKZCVHLZVEVPCVHVEVKVHEZVKAUBIUCIZEZVPSZVPVEVRVK | ||
| AVJJKZBVSUDZEWAVEVHWCVKBAUJUEWBVPBVKVSVJVKAJUFUGUHVTVPUIUKULVMVQBADVJAUMV | ||
| LVPCVHVJAVKJUNUOUPUQVOVFTEZVHTEZSVGVIVNURWDWEAUSAHVAUTBCVFVHVBVCVD $. | ||
| $} | ||
|
|
There was a problem hiding this comment.
Note: it looks like these were deleted since they were duplicates of ssltleft and ssltright
icecream17
approved these changes
Aug 19, 2024
tirix
reviewed
Aug 20, 2024
set.mm
Outdated
Comment on lines
530705
to
530708
| $( A surreal is part of a made set iff its birthday is less than or equal | ||
| to that ordinal. (Contributed by Scott Fenton, 19-Aug-2024.) $) | ||
| madebday $p |- ( ( A e. On /\ X e. No ) -> ( X e. ( _M ` A ) <-> | ||
| ( bday ` X ) C_ A ) ) $= |
There was a problem hiding this comment.
Maybe it's because I'm not versed into surreal numbers, but at first I could not guess which that ordinal was, since no ordinal was mentioned before. Would it make sense to write:
A surreal is part of the set made by ordinal
Aiff its birthday is less than or equal toA
?
There was a problem hiding this comment.
Good point. That's done now.
tirix
approved these changes
Aug 20, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
More work on surreals - proved biconditional madebday and oldbday.
Moved rabeqdca to main set.mm