Documentation

LeanPool.MisereGames.Misere.ShortIncomparable

Misere combinatorial games.

Short Sets and Comparison #

This is a mirror of CombinatorialGames.Misere.LiftIncomparable module with the difference that if we are in a short universe then we do not need to increase the universe level.

The main results are

source
noncomputable def MisereGames.AugmentedForm.Short.adjointsOfShort :
Set AugmentedForm

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

Equations
Instances For
    source
    instance MisereGames.AugmentedForm.Short.smallShortAdjoints :
    Small.{u, u + 1} ↑adjointsOfShort
    source
    noncomputable def MisereGames.AugmentedForm.Short.g :
    AugmentedForm

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

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

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MisereGames.AugmentedForm.Short.adjoint_mem_adjointsOfShort {X : AugmentedForm} (hX : Form.IsShort X) :
        X° ∈ adjointsOfShort
        source
        @[simp]
        theorem MisereGames.AugmentedForm.Short.moves_g (p : Player) :
        Moves.moves p g = adjointsOfShort
        source
        @[simp]
        theorem MisereGames.AugmentedForm.Short.moves_h (p : Player) :
        Moves.moves p h = insert g adjointsOfShort
        source
        theorem MisereGames.AugmentedForm.Short.bigG_not_isEndLike (p : Player) :
        ¬Form.IsEndLike p g
        source
        theorem MisereGames.AugmentedForm.Short.bigH_not_isEndLike (p : Player) :
        ¬Form.IsEndLike p h
        source
        theorem MisereGames.AugmentedForm.Short.misereOutcome_g_add_short {x : AugmentedForm} (h_isShort : Form.IsShort x) :
        Form.Misere.Outcome.MisereOutcome (g + x) = Outcome.N
        source
        theorem MisereGames.AugmentedForm.Short.misereOutcome_h_add_short {x : AugmentedForm} (h_isShort : Form.IsShort x) :
        Form.Misere.Outcome.MisereOutcome (h + x) = Outcome.N
        source
        theorem MisereGames.AugmentedForm.Short.g_not_isEndLike (p : Player) :
        ¬Form.IsEndLike p g
        source
        theorem MisereGames.AugmentedForm.Short.misereOutcome_g_add_g :
        Form.Misere.Outcome.MisereOutcome (g + g) = Outcome.P
        source
        theorem MisereGames.AugmentedForm.Short.misereOutcome_h_add_g :
        Form.Misere.Outcome.MisereOutcome (h + g) = Outcome.N
        source
        theorem MisereGames.AugmentedForm.Short.g_misereEQ_h_short (A : AugmentedForm → Prop) (h_short : ∀ (x : AugmentedForm), A x → Form.IsShort x) :
        g =m A h
        source
        theorem MisereGames.AugmentedForm.Short.g_misereEQ_h_shortUniverse (U : AugmentedForm → Prop) [ShortUniverse U] :
        g =m U h
        source
        theorem MisereGames.AugmentedForm.Short.g_h_incomparable {A : AugmentedForm → Prop} (h_Ag : A g) :
        ¬g ≥m A h ∧ ¬h ≥m A g
        source
        theorem MisereGames.AugmentedForm.Short.g_mem_longUniverse (U : AugmentedForm → Prop) [LongUniverse U] :
        U g

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

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