moveRight_mk_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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