moveLeft_mk_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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