English
For constructors mk xl xr xL xR and mk yl yr yL yR, the left-Forward relation between the constructed games is equivalent to a disjunction of the existence of a move in the left branch or the existence of a move in the right branch, both expressed using the ≤ relation. Specifically, LF(mk xl xr xL xR, mk yl yr yL yR) iff ∃ i, mk xl xr xL xR ≤ yL i or ∃ j, xR j ≤ mk yl yr yL yR.
Русский
Для конструкторов mk xl xr xL xR и mk yl yr yL yR, отношение LF между полученными играми эквивалентно дизъюнкции существования хода в левой ветви или существования хода в правой ветви, выраженной через ≤.
LaTeX
$$$ (\\mathrm{mk}_{xl,xr,xL,xR}) \\mathrm{LF} (\\mathrm{mk}_{yl,yr,yL,yR}) \\iff (\\exists i: xl, \\mathrm{mk}_{xl,xr,xL,xR} ≤ yL i) \\lor (\\exists j: yr, xR j ≤ \\mathrm{mk}_{yl,yr,yL,yR}). $$$
Lean4
/-- Definition of `x ⧏ y` on pre-games built using the constructor. -/
@[simp]
theorem mk_lf_mk {xl xr xL xR yl yr yL yR} :
mk xl xr xL xR ⧏ mk yl yr yL yR ↔ (∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR :=
lf_iff_exists_le
