moveLeft_mk_right — Mathlib

English

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

Русский

Для любых xL, i и xR переход влево внутри правой части образует последующий относительно mk xl xr xL xR.

LaTeX

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

Lean4

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

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