mk_right — Mathlib

English

For any xl, xr, and xL, xR, the right component xR(i) is a subsequent of the composite mk xl xr xL xR for i in xr.

Русский

Для любых xl, xr и функций xL, xR правая компонента xR(i) является последующим относительно образованной игры mk xl xr xL xR на i ∈ xr.

LaTeX

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

Lean4

@[simp]
theorem mk_right {xl xr} (xL : xl → PGame) (xR : xr → PGame) (j : xr) : Subsequent (xR j) (mk xl xr xL xR) :=
  @Subsequent.moveRight (mk _ _ _ _) j

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