Documentation

CombinatorialGames.Game.Loopy.IGame

Well-founded games to loopy games #

We define the embedding IGame ↪ LGame, and prove that it behaves in the expected ways with arithmetic.

def IGame.toLGame :

IGame ↪ LGame

The inclusion map from well-founded games into loopy games.

Equations

IGame.toLGame = { toFun := IGame.toLGame'✝, inj' := ⋯ }

Instances For

instance IGame.instCoeLGame :

Coe IGame LGame

Equations

IGame.instCoeLGame = { coe := ⇑IGame.toLGame }

theorem IGame.toLGame_def (x : IGame) :

toLGame x = {⇑toLGame '' x.leftMoves | ⇑toLGame '' x.rightMoves}ᴸ

@[simp]

theorem IGame.leftMoves_toLGame (x : IGame) :

(toLGame x).leftMoves = ⇑toLGame '' x.leftMoves

@[simp]

theorem IGame.rightMoves_toLGame (x : IGame) :

(toLGame x).rightMoves = ⇑toLGame '' x.rightMoves

theorem IGame.acc_toLGame (x : IGame) :

Acc LGame.IsOption (toLGame x)

theorem IGame.mem_range_toLGame_iff_acc {x : LGame} :

x ∈ Set.range ⇑toLGame ↔ Acc LGame.IsOption x

@[simp]

theorem IGame.toLGame_zero :

@[simp]

theorem IGame.toLGame_one :

@[simp, irreducible]

theorem IGame.toLGame_neg (x : IGame) :

toLGame (-x) = -toLGame x

@[simp, irreducible]

theorem IGame.toLGame_add (x y : IGame) :

toLGame (x + y) = toLGame x + toLGame y

@[simp]

theorem IGame.toLGame_sub (x y : IGame) :

toLGame (x - y) = toLGame x - toLGame y

@[simp, irreducible]

theorem IGame.toLGame_mul (x y : IGame) :

toLGame (x * y) = toLGame x * toLGame y

@[simp]

theorem IGame.toLGame_mulOption (x y a b : IGame) :

toLGame (mulOption x y a b) = LGame.mulOption (toLGame x) (toLGame y) (toLGame a) (toLGame b)