moveRight — Mathlib

English

For any x, and any right move j of x, the move to the right yields a subsequent position relative to x.

Русский

Для любого x и любого правого хода j из x переход к правому ходу образует последующий по отношению к x.

LaTeX

$$$\forall x:\mathrm{PGame},\forall j:\!x.\mathrm{RightMoves},\ (x.\mathrm{moveRight} j).\mathrm{Subsequent} x.$$$

Lean4

@[simp]
theorem moveRight {x : PGame} (j : x.RightMoves) : Subsequent (x.moveRight j) x :=
  TransGen.single (IsOption.moveRight j)

Похожие утверждения