mk_right' — Mathlib

English

A variant of mk_right asserting that for any RightMoves j of the mk xl xr xL xR, the position (xR j) is a subsequent to that mk game.

Русский

Вариант mk_right', утверждающий, что для любых RightMoves j образованной mk xl xr xL xR, положение (xR j) является последующим относительно этой игры mk.

LaTeX

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

Lean4

@[simp]
theorem mk_right' (xL : xl → PGame) (xR : xr → PGame) (j : RightMoves (mk xl xr xL xR)) :
    Subsequent (xR j) (mk xl xr xL xR) := by pgame_wf_tac

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