Documentation

LeanPool.MisereGames.AugmentedForm.Lift

Misere combinatorial games.

source
@[irreducible]
noncomputable def MisereGames.AugmentedForm.liftSucc (g : AugmentedForm) :
AugmentedForm

Lift an augmented form to the next universe level.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem MisereGames.AugmentedForm.moves_liftSucc (p : Player) (g : AugmentedForm) :
    Moves.moves p g.liftSucc = liftSucc '' Moves.moves p g
    source
    @[simp]
    theorem MisereGames.AugmentedForm.hasTombstone_liftSucc (p : Player) (g : AugmentedForm) :
    hasTombstone p g.liftSucc ↔ hasTombstone p g
    source
    theorem MisereGames.AugmentedForm.liftSucc_injective :
    Function.Injective liftSucc
    source
    @[simp]
    theorem MisereGames.AugmentedForm.isEnd_liftSucc (p : Player) (g : AugmentedForm) :
    Form.IsEnd p g.liftSucc ↔ Form.IsEnd p g
    source
    @[simp]
    theorem MisereGames.AugmentedForm.isEndLike_liftSucc (p : Player) (g : AugmentedForm) :
    Form.IsEndLike p g.liftSucc ↔ Form.IsEndLike p g
    source
    @[simp]
    theorem MisereGames.AugmentedForm.liftSucc_add (a b : AugmentedForm) :
    (a + b).liftSucc = a.liftSucc + b.liftSucc
    source
    @[simp]
    theorem MisereGames.AugmentedForm.winsGoingFirst_liftSucc (p : Player) (g : AugmentedForm) :
    Form.Misere.Outcome.WinsGoingFirst p g.liftSucc ↔ Form.Misere.Outcome.WinsGoingFirst p g
    source
    @[simp]
    theorem MisereGames.AugmentedForm.misereOutcome_liftSucc (g : AugmentedForm) :
    Form.Misere.Outcome.MisereOutcome g.liftSucc = Form.Misere.Outcome.MisereOutcome g
    source
    @[simp]
    theorem MisereGames.AugmentedForm.liftSucc_zero :
    liftSucc 0 = 0
    source
    @[simp]
    theorem MisereGames.AugmentedForm.not_hasTombstone_adjoint {p : Player} {g : AugmentedForm} :
    ¬hasTombstone p (g°)
    source
    @[simp]
    theorem MisereGames.AugmentedForm.liftSucc_adjoint (g : AugmentedForm) :
    g°.liftSucc = g.liftSucc°