Surreal cuts #
A surreal cut is defined as consisting of two sets of surreals with the following properties:
- They are complementary sets.
- Every surreal in the first set is less than every surreal in the second set.
This construction resembles the construction of the surreals themselves, but yields a "bigger" structure, which can embed the surreals, but is also a complete linear order.
Note that surreal cuts are is not the same as the Dedekind completion of the surreals. Whereas
the Dedekind completion maps every element of the original order to a unique Dedekind cut, every
surreal number x
actually corresponds to two cuts (Iio x, Ici x)
and (Iic x, Ioi x)
, which we
call the left and right cut, respectively.
The theory of concept lattices gives us a very simple definition of surreal cuts as
Concept Surreal Surreal (⬝ < ⬝)
. However, we've attempted to provide a thin wrapper for all
concept terminology.
A surreal cut consists of two complementary sets of surreals, where every surreal in the former is less than every surreal in the latter.
Instances For
Basic definitions #
The left set in a cut. This is an alias for Concept.extent
.
Instances For
The right set in a cut. This is an alias for Concept.intent
.
Instances For
Alias of Concept.disjoint_extent_intent
.
Note that if r'
is the ≤
relation, this theorem will often not be true!
Alias of Concept.codisjoint_extent_intent
.
Alias of Concept.isCompl_extent_intent
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Surreal.Cut.instInvolutiveNeg = { toNeg := Surreal.Cut.instNeg, neg_neg := Surreal.Cut.instInvolutiveNeg._proof_1 }
Cuts from games #
The left cut of a game x
is such that its right set consists of surreals
equal or larger to it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The right cut of a game x
is such that its right set consists of surreals
equal or lesser to it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cut just to the left of a surreal number.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cut just to the right of a surreal number.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Calculating cuts #
The supremum of all right cuts of left options of x
.
If infRight x ≤ supLeft x
then leftGame x = supLeft x
and rightGame x = infRight x
; otherwise,
x
is equivalent to the simplest surreal between supLeft x
and infRight x
.
Equations
- Surreal.Cut.supLeft x = ⨆ i ∈ x.leftMoves, Surreal.Cut.rightGame (Game.mk i)
Instances For
The infimum of all left cuts of right options of x
.
If infRight x ≤ supLeft x
then leftGame x = supLeft x
and rightGame x = infRight x
; otherwise,
x
is equivalent to the simplest surreal between supLeft x
and infRight x
.
Equations
- Surreal.Cut.infRight x = ⨅ i ∈ x.rightMoves, Surreal.Cut.leftGame (Game.mk i)
Instances For
The simplest surreal number (in terms of birthday) that fits between two cuts.