lf_mk — Mathlib

English

For any xL, xR, i, the left component xL i is LF relative to the whole game mk xl xr xL xR.

Русский

Для любых xL, xR, i левая часть xL i является LF по отношению к mk xl xr xL xR.

LaTeX

$$$$ \\forall {xl xr} \\; (xL : xl \\to PGame) \\; (xR : xr \\to PGame) \\; (i) : xL i \\\\mathbf{LF} (mk xl xr xL xR). $$$$

Lean4

theorem lf_mk {xl xr} (xL : xl → PGame) (xR : xr → PGame) (i) : xL i ⧏ mk xl xr xL xR :=
  @moveLeft_lf (mk _ _ _ _) i

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