mk_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mk_left {xl xr} (xL : xl → PGame) (xR : xr → PGame) (i : xl) : Subsequent (xL i) (mk xl xr xL xR) :=
  @Subsequent.moveLeft (mk _ _ _ _) i

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