mk_right — Mathlib

English

Let xl and xr be types, xL : xl → PGame and xR : xr → PGame. For any i ∈ xr, the game xR(i) is a right option of the composite mk xl xr xL xR.

Русский

Пусть xl, xr — множества индексов, xL : xl → PGame и xR : xr → PGame. Для любого i ∈ xr игра xR(i) является правым вариантом образованной игры mk xl xr xL xR.

LaTeX

$$$\forall xl\ xr:\n\text{Type},\ xL: xl \to \mathrm{PGame},\ xR: xr \to \mathrm{PGame},\ i:\ xr,\ (xR i) \text{ является правым вариантом } \mathrm{mk}\ xl\ xr\ xL\ xR.$$$

Lean4

theorem mk_right {xl xr : Type u} (xL : xl → PGame) (xR : xr → PGame) (i : xr) : (xR i).IsOption (mk xl xr xL xR) :=
  @IsOption.moveRight (mk _ _ _ _) i

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