mk_lf_of_le — Mathlib

English

If there exists an i such that xR j ≤ y for all j, then mk xl xr xL xR is Left-Following to y; equivalently, whenever some xR j ≤ y, we have mk xl xr xL xR ⧏ y.

Русский

Если существует j такой, что xR j ≤ y, то mk xl xr xL xR ⧏ y.

LaTeX

$$$\\\\forall {xl xr} \\, {y : PGame} \\, (xR : xr \\\\to PGame) \\\\Rightarrow \\\\forall i \\, (xR j \\\\le y) \\\\Rightarrow mk xl xr xL xR \\\\mathbf{⧏} y.$$$

Lean4

theorem mk_lf_of_le {xl xr y j} (xL) {xR : xr → PGame} : xR j ≤ y → mk xl xr xL xR ⧏ y :=
  @lf_of_moveRight_le (mk _ _ _ _) y j

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