Documentation

CombinatorialGames.AugmentedForm.Lift

@[irreducible]

noncomputable def AugmentedForm.liftSucc (g : AugmentedForm) :

Equations

g.liftSucc = AugmentedForm.ofSetsWithTombs (fun (p : Player) => Set.range fun (y : ↑(Moves.moves p g)) => (↑y).liftSucc) fun (p : Player) => AugmentedForm.hasTombstone p g

Instances For

@[simp]

theorem AugmentedForm.moves_liftSucc (p : Player) (g : AugmentedForm) :

Moves.moves p g.liftSucc = liftSucc '' Moves.moves p g

@[simp]

theorem AugmentedForm.hasTombstone_liftSucc (p : Player) (g : AugmentedForm) :

hasTombstone p g.liftSucc ↔ hasTombstone p g

theorem AugmentedForm.liftSucc_injective :

Function.Injective liftSucc

@[simp]

theorem AugmentedForm.isEnd_liftSucc (p : Player) (g : AugmentedForm) :

Form.IsEnd p g.liftSucc ↔ Form.IsEnd p g

@[simp]

theorem AugmentedForm.isEndLike_liftSucc (p : Player) (g : AugmentedForm) :

Form.IsEndLike p g.liftSucc ↔ Form.IsEndLike p g

@[simp]

theorem AugmentedForm.liftSucc_add (a b : AugmentedForm) :

(a + b).liftSucc = a.liftSucc + b.liftSucc

@[simp]

theorem AugmentedForm.winsGoingFirst_liftSucc (p : Player) (g : AugmentedForm) :

Form.Misere.Outcome.WinsGoingFirst p g.liftSucc ↔ Form.Misere.Outcome.WinsGoingFirst p g

@[simp]

theorem AugmentedForm.misereOutcome_liftSucc (g : AugmentedForm) :

Form.Misere.Outcome.MisereOutcome g.liftSucc = Form.Misere.Outcome.MisereOutcome g

@[simp]

theorem AugmentedForm.liftSucc_zero :

@[simp]

theorem AugmentedForm.not_hasTombstone_adjoint {p : Player} {g : AugmentedForm} :

¬hasTombstone p (g°)

@[simp]

theorem AugmentedForm.liftSucc_adjoint (g : AugmentedForm) :

g°.liftSucc = g.liftSucc°