Metamath Proof Explorer


Table of Contents - 15.1. Sign sequence representation and Alling's axioms

The surreal numbers can be represented in several equivalent ways. In [Alling], Norman Alling made this notion explicit by giving a set of axioms that all representations admit, then proving that there is an order and birthday preserving bijection between any systems that satisfy these axioms.

In this section, we start with the definition of surreal numbers given in [Gonshor] and derive Alling's axioms. After deriving them we no longer refer to the explicit definition of surreals. In particular, we never take advantage of the fact that the empty set is a surreal number under our definition.

  1. Definitions and initial properties
    1. csur
    2. clts
    3. cbday
    4. df-no
    5. df-lts
    6. df-bday
    7. elno
    8. elnoOLD
    9. ltsval
    10. bdayval
    11. nofun
    12. nodmon
    13. norn
    14. nofnbday
    15. nodmord
    16. elno2
    17. elno3
    18. ltsval2
    19. nofv
    20. nosgnn0
    21. nosgnn0i
    22. noreson
    23. ltsintdifex
    24. ltsres
    25. noxp1o
    26. noseponlem
    27. nosepon
    28. noextend
    29. noextendseq
    30. noextenddif
    31. noextendlt
    32. noextendgt
    33. nolesgn2o
    34. nolesgn2ores
    35. nogesgn1o
    36. nogesgn1ores
  2. Ordering
    1. ltssolem1
    2. ltsso
  3. Birthday Function
    1. bdayfo
  4. Density
    1. fvnobday
    2. nosepnelem
    3. nosepne
    4. nosep1o
    5. nosep2o
    6. nosepdmlem
    7. nosepdm
    8. nosepeq
    9. nosepssdm
    10. nodenselem4
    11. nodenselem5
    12. nodenselem6
    13. nodenselem7
    14. nodenselem8
    15. nodense
  5. Full-Eta Property
    1. bdayimaon
    2. nolt02olem
    3. nolt02o
    4. nogt01o
    5. noresle
    6. nomaxmo
    7. nominmo
    8. nosupprefixmo
    9. noinfprefixmo
    10. nosupcbv
    11. nosupno
    12. nosupdm
    13. nosupbday
    14. nosupfv
    15. nosupres
    16. nosupbnd1lem1
    17. nosupbnd1lem2
    18. nosupbnd1lem3
    19. nosupbnd1lem4
    20. nosupbnd1lem5
    21. nosupbnd1lem6
    22. nosupbnd1
    23. nosupbnd2lem1
    24. nosupbnd2
    25. noinfcbv
    26. noinfno
    27. noinfdm
    28. noinfbday
    29. noinffv
    30. noinfres
    31. noinfbnd1lem1
    32. noinfbnd1lem2
    33. noinfbnd1lem3
    34. noinfbnd1lem4
    35. noinfbnd1lem5
    36. noinfbnd1lem6
    37. noinfbnd1
    38. noinfbnd2lem1
    39. noinfbnd2
    40. nosupinfsep
    41. noetasuplem1
    42. noetasuplem2
    43. noetasuplem3
    44. noetasuplem4
    45. noetainflem1
    46. noetainflem2
    47. noetainflem3
    48. noetainflem4
    49. noetalem1
    50. noetalem2
    51. noeta