lf_of_le_mk — Mathlib

English

Let xl, xr be index sets and xL : xl → PGame, xR : xr → PGame. If the manufactured game mk xl xr xL xR is less than or equal to y, then every left option xL i is strictly to the left of y, i.e. xL(i) ⧏ y for all i.

Русский

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

LaTeX

$$$\\\\forall xl xr \\, xL \\\\colon xl \\\\to PGame \\\\to \\\\forall i \\, xL i \\\\mathbf{⧏} y \\\\text{ whenever } mk xl xr xL xR \\\\le y.$$$

Lean4

theorem lf_of_le_mk {xl xr xL xR y} : mk xl xr xL xR ≤ y → ∀ i, xL i ⧏ y :=
  moveLeft_lf_of_le

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