Documentation

LeanPool.MisereGames.Misere.LiftIncomparable

Misere combinatorial games.

Lifting Sets and Comparison #

The main results are

source
noncomputable def MisereGames.AugmentedForm.adjointsOfSmall :
Set AugmentedForm

The set of all adjoints $J^\circ$ (lifted to $u + 1$) for all $J$ in universe $u$.

Equations
Instances For
    source
    instance MisereGames.AugmentedForm.smallAdjointsOfSmall :
    Small.{u + 1, u + 2} ↑adjointsOfSmall
    source
    noncomputable def MisereGames.AugmentedForm.g :
    AugmentedForm

    $G = \{ J^\circ \mid J^\circ \}$ for all $J$ in universe $u$.

    Equations
    Instances For
      source
      instance MisereGames.AugmentedForm.smallInsertG :
      Small.{u + 1, u + 2} ↑(insert g adjointsOfSmall)
      source
      noncomputable def MisereGames.AugmentedForm.h :
      AugmentedForm

      $H = \{ G, J^\circ \mid G, J^\circ \}$ for all $J$ in universe $u$.

      Equations
      Instances For
        source
        @[simp]
        theorem MisereGames.AugmentedForm.moves_g (p : Player) :
        Moves.moves p g = adjointsOfSmall
        source
        @[simp]
        theorem MisereGames.AugmentedForm.moves_h (p : Player) :
        Moves.moves p h = insert g adjointsOfSmall
        source
        theorem MisereGames.AugmentedForm.liftAdjoint_mem_adjointsOfSmall (x : AugmentedForm) :
        x°.liftSucc ∈ adjointsOfSmall
        source
        theorem MisereGames.AugmentedForm.g_not_isEndLike (p : Player) :
        ¬Form.IsEndLike p g
        source
        theorem MisereGames.AugmentedForm.misereOutcome_add_liftSucc_adjoint_eq_P (x : AugmentedForm) :
        Form.Misere.Outcome.MisereOutcome (x.liftSucc + x°.liftSucc) = Outcome.P

        The sum of a (lifted) adjoint and its base game is a $\mathscr{P}$-position.

        source
        theorem MisereGames.AugmentedForm.misereOutcome_g_add_lift (x : AugmentedForm) :
        Form.Misere.Outcome.MisereOutcome (g + x.liftSucc) = Outcome.N

        For all games in universe $u$ and $G$ in $u + 1$, $\operatorname{o}(G + X) = \mathscr{N}$.

        source
        theorem MisereGames.AugmentedForm.misereOutcome_h_add_lift (x : AugmentedForm) :
        Form.Misere.Outcome.MisereOutcome (h + x.liftSucc) = Outcome.N

        For all games in universe $u$ and $H$ in $u + 1$, $\operatorname{o}(G + X) = \mathscr{N}$.

        source
        def MisereGames.AugmentedForm.liftSet (A : AugmentedForm → Prop) :
        AugmentedForm → Prop

        Lift a set on AugmentedForm.{u} to one on AugmentedForm.{u + 1} via the range of AugmentedForm.liftSucc.

        Equations
        Instances For
          source
          theorem MisereGames.AugmentedForm.g_misereEQ_h_lift (A : AugmentedForm → Prop) :
          g =m (liftSet A)h

          If $G, H$ are in universe $u$ then there are indistinguishable modulo set $\mathcal{A}$ lifted to $u + 1$.

          source
          theorem MisereGames.AugmentedForm.misereOutcome_g_add_g :
          Form.Misere.Outcome.MisereOutcome (g + g) = Outcome.P

          $o(G + G) = \mathscr{P}$

          source
          theorem MisereGames.AugmentedForm.misereOutcome_h_add_g :
          Form.Misere.Outcome.MisereOutcome (h + g) = Outcome.N

          $\operatorname{o}(H + G) = \mathscr{N}$.

          source
          theorem MisereGames.AugmentedForm.g_h_incomparable {A : AugmentedForm → Prop} (h_Ag : A g) :
          ¬g ≥m A h ∧ ¬h ≥m A g

          $G$ and $H$ are incomparable modulo any set $\mathcal{A}$ in $u + 1$.

          source
          theorem MisereGames.AugmentedForm.g_mem_longUniverse (U : AugmentedForm → Prop) [LongUniverse U] :
          U g

          $G$ is in any universe $\mathcal{U}$ in $u + 1$.

          source
          theorem MisereGames.AugmentedForm.g_h_incomparable_longUniverse (U : AugmentedForm → Prop) [LongUniverse U] :
          ¬g ≥m U h ∧ ¬h ≥m U g

          $G$ and $H$ are incomparable modulo any universe $\mathcal{U}$ in $u + 1$.