mk_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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