Documentation

CombinatorialGames.Surreal.Cut

Surreal cuts #

A surreal cut is defined as consisting of two sets of surreals with the following properties:

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.

@[reducible, inline]
abbrev Surreal.Cut :
Type (u_1 + 1)

A surreal cut consists of two complementary sets of surreals, where every surreal in the former is less than every surreal in the latter.

Equations
Instances For

    Basic definitions #

    The left set in a cut. This is an alias for Concept.extent.

    Equations
    Instances For

      The right set in a cut. This is an alias for Concept.intent.

      Equations
      Instances For
        theorem Surreal.Cut.left_lt_right {α : Type u_2} {β : Type u_3} {r : αβProp} {c : Concept α β r} {x : α} {y : β} (hx : x c.extent) (hy : y c.intent) :
        r x y

        Alias of Concept.rel_extent_intent.

        theorem Surreal.Cut.disjoint_left_right {α : Type u_2} {r' : ααProp} [IsIrrefl α r'] (c' : Concept α α r') :

        Alias of Concept.disjoint_extent_intent.


        Note that if r' is the relation, this theorem will often not be true!

        theorem Surreal.Cut.codisjoint_left_right {α : Type u_2} {r' : ααProp} [IsTrichotomous α r'] [IsTrans α r'] (c' : Concept α α r') :

        Alias of Concept.codisjoint_extent_intent.

        theorem Surreal.Cut.isCompl_left_right {α : Type u_2} {r' : ααProp} [IsStrictTotalOrder α r'] (c' : Concept α α r') :

        Alias of Concept.isCompl_extent_intent.

        theorem Surreal.Cut.ext {c d : Cut} (h : c.left = d.left) :
        c = d
        theorem Surreal.Cut.ext_iff {c d : Cut} :
        c = d c.left = d.left
        theorem Surreal.Cut.ext' {c d : Cut} (h : c.right = d.right) :
        c = d
        @[simp]
        theorem Surreal.Cut.left_inj {c d : Cut} :
        c.left = d.left c = d
        @[simp]
        theorem Surreal.Cut.right_inj {c d : Cut} :
        c.right = d.right c = d
        @[simp]
        @[simp]
        @[simp]
        @[simp]
        @[simp]
        theorem Surreal.Cut.notMem_left_iff {x : Cut} {y : Surreal} :
        yx.left y x.right
        @[simp]
        theorem Surreal.Cut.notMem_right_iff {x : Cut} {y : Surreal} :
        yx.right y x.left
        instance Surreal.Cut.instIsTotalLe :
        IsTotal Cut fun (x1 x2 : Cut) => x1 x2
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem Surreal.Cut.left_min (x y : Cut) :
        (min x y).left = x.left y.left
        @[simp]
        theorem Surreal.Cut.right_min (x y : Cut) :
        (min x y).right = x.right y.right
        @[simp]
        theorem Surreal.Cut.right_max (x y : Cut) :
        (max x y).right = x.right y.right
        @[simp]
        theorem Surreal.Cut.left_max (x y : Cut) :
        (max x y).left = x.left y.left
        @[simp]
        theorem Surreal.Cut.left_sInf (s : Set Cut) :
        (sInf s).left = xs, x.left
        @[simp]
        theorem Surreal.Cut.right_sInf (s : Set Cut) :
        (sInf s).right = xs, x.right
        @[simp]
        theorem Surreal.Cut.right_sSup (s : Set Cut) :
        (sSup s).right = xs, x.right
        @[simp]
        theorem Surreal.Cut.left_sSup (s : Set Cut) :
        (sSup s).left = xs, x.left
        @[simp]
        theorem Surreal.Cut.left_iInf {ι : Sort u_1} (f : ιCut) :
        (⨅ (i : ι), f i).left = ⋂ (i : ι), (f i).left
        @[simp]
        theorem Surreal.Cut.right_iInf {ι : Sort u_1} (f : ιCut) :
        (⨅ (i : ι), f i).right = ⋃ (i : ι), (f i).right
        @[simp]
        theorem Surreal.Cut.right_iSup {ι : Sort u_1} (f : ιCut) :
        (⨆ (i : ι), f i).right = ⋂ (i : ι), (f i).right
        @[simp]
        theorem Surreal.Cut.left_iSup {ι : Sort u_1} (f : ιCut) :
        (⨆ (i : ι), f i).left = ⋃ (i : ι), (f i).left
        Equations
        @[simp]
        theorem Surreal.Cut.left_neg (x : Cut) :
        (-x).left = -x.right
        @[simp]
        theorem Surreal.Cut.right_neg (x : Cut) :
        (-x).right = -x.left
        @[simp]
        theorem Surreal.Cut.neg_min (x y : Cut) :
        -min x y = max (-x) (-y)
        @[simp]
        theorem Surreal.Cut.neg_max (x y : Cut) :
        -max x y = min (-x) (-y)
        @[simp]
        theorem Surreal.Cut.neg_sInf (s : Set Cut) :
        -sInf s = sSup (-s)
        @[simp]
        theorem Surreal.Cut.neg_sSup (s : Set Cut) :
        -sSup s = sInf (-s)
        @[simp]
        theorem Surreal.Cut.neg_iInf {ι : Sort u_1} (f : ιCut) :
        -⨅ (i : ι), f i = ⨆ (i : ι), -f i
        @[simp]
        theorem Surreal.Cut.neg_iSup {ι : Sort u_1} (f : ιCut) :
        -⨆ (i : ι), f i = ⨅ (i : ι), -f i
        @[simp]
        theorem Surreal.Cut.neg_le_neg_iff {x y : Cut} :
        -x -y y x
        theorem Surreal.Cut.neg_le {x y : Cut} :
        -x y -y x
        theorem Surreal.Cut.le_neg {x y : Cut} :
        x -y y -x
        @[simp]
        theorem Surreal.Cut.neg_lt_neg_iff {x y : Cut} :
        -x < -y y < x
        theorem Surreal.Cut.neg_lt {x y : Cut} :
        -x < y -y < x
        theorem Surreal.Cut.lt_neg {x y : Cut} :
        x < -y y < -x

        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
                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
                  Instances For
                    def Surreal.Cut.Fits (x : Surreal) (y z : Cut) :

                    A surreal x fits between two cuts y and z when x ∈ y.right ∩ z.left.

                    Equations
                    Instances For
                      theorem Surreal.Cut.Fits.lt {x : Surreal} {y z : Cut} (h : Fits x y z) :
                      y < z
                      theorem Surreal.Cut.Fits.le_leftSurreal {x : Surreal} {y z : Cut} (h : Fits x y z) :
                      theorem Surreal.Cut.not_fits_iff {x : Surreal} {y z : Cut} :
                      ¬Fits x y z x y.left z.right
                      noncomputable def Surreal.Cut.simplestBtwn {x y : Cut} (h : x < y) :

                      The simplest surreal number (in terms of birthday) that fits between two cuts.

                      Equations
                      Instances For
                        theorem Surreal.Cut.fits_simplestBtwn {x y : Cut} (h : x < y) :

                        If x is a game with supLeft x < infRight x, then the simplest number between those two cuts is equal to x.