moveRight_mk_right — Mathlib

English

For any xL, i, and xR, the game ((xR i).moveRight j) is a subsequent of the composite mk xl xr xL xR for any j in (RightMoves of xR i).

Русский

Для любых xL, i и xR переход вправо внутри правой части образует последующий по отношению к mk xl xr xL xR для любого j в RightMoves (xR i).

LaTeX

$$$\forall {xL : \text{xl} \to \mathrm{PGame}} {i} (xR : \text{xr} \to \mathrm{PGame}) (j),\ ((xR i).moveRight j)\ \mathrm{Subsequent}\ (\mathrm{mk}\ xl xr xL xR).$$$

Lean4

@[simp]
theorem moveRight_mk_right {xL : xl → PGame} {i : xr} (xR : xr → PGame) (j) :
    Subsequent ((xR i).moveRight j) (mk xl xr xL xR) := by pgame_wf_tac

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