lf_of_mk_le — Mathlib

English

If x ≤ mk yl yr yL yR, then for every j, x.LF (yR j). In other words, x is left-following to each right-move of the right-side component.

Русский

Если x ≤ mk yl yr yL yR, то для каждого j выполняется x LF (yR j). То есть x идёт слева по отношению к каждому правому ходу правой части.

LaTeX

$$$\\\\forall {xl xr} \\, {xL} \\\\colon xl \\\\to PGame, {xR} \\\\colon xr \\\\to PGame \\\\to x \\\\le mk yl yr yL yR \\\\Rightarrow \\\\forall j, x \\\\mathbf{⧏} (yR j).$$$

Lean4

theorem lf_of_mk_le {x yl yr yL yR} : x ≤ mk yl yr yL yR → ∀ j, x ⧏ yR j :=
  lf_moveRight_of_le

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