English
For pre-games built by the mk constructor, the ≤ relation is characterized by left and right move exposure: mk xl xr xL xR ≤ mk yl yr yL yR holds iff every left move is lf to the right-hand, and the constructed game is lf to the corresponding right move of y.
Русский
Для конструированных через mk прเกมов, отношение ≤ описывается через левый и правый ходы: mk xl xr xL xR ≤ mk yl yr yL yR тогда и только тогда, когда все левые ходы LF к mk yl yr yL yR, и mk xl xr xL xR LF к каждому правому ходу yR j.
LaTeX
$$$\text{mk}\ xl xr\ xL xR \le \text{mk}\ yl yr\ yL yR \iff (\forall i, xL i \;⧏\; \text{mk}\ yl yr yL yR) \land (\forall j, \text{mk}\ xl xr xL xR \;⧏\; yR j)$$$
Lean4
/-- Definition of `x ≤ y` on pre-games built using the constructor. -/
@[simp]
theorem mk_le_mk {xl xr xL xR yl yr yL yR} :
mk xl xr xL xR ≤ mk yl yr yL yR ↔ (∀ i, xL i ⧏ mk yl yr yL yR) ∧ ∀ j, mk xl xr xL xR ⧏ yR j :=
le_iff_forall_lf
