English
PGame equipped with ≤ forms a preorder: reflexive and transitive; and define x < y as x ≤ y and x ⧏ y.
Русский
Обозначение ≤ на PGame образует полную предорядок: рефлексивность и транзитивность; определим x < y как x ≤ y и x ⧏ y.
LaTeX
$$$$ x \le x \quad\\land\\quad x \le y \\land y \le z \\Rightarrow x \le z \\\\text{ и } x < y \\Leftrightarrow (x \le y) \\land (x ⧏ y). $$$$
Lean4
instance : Preorder PGame :=
{
PGame.le with
le_refl := fun x =>
by
induction x with
| mk _ _ _ _ IHl IHr => _
exact le_of_forall_lf (fun i => lf_of_le_moveLeft (IHl i)) fun i => lf_of_moveRight_le (IHr i)
le_trans :=
by
suffices ∀ {x y z : PGame}, (x ≤ y → y ≤ z → x ≤ z) ∧ (y ≤ z → z ≤ x → y ≤ x) ∧ (z ≤ x → x ≤ y → z ≤ y) from
fun x y z => this.1
intro x y z
induction x generalizing y z with
| _ xl xr xL xR IHxl IHxr
induction y generalizing z with
| _ yl yr yL yR IHyl IHyr
induction z with
| _ zl zr zL zR IHzl IHzr
exact
⟨le_trans_aux (fun {i} => (IHxl i).2.1) fun {j} => (IHzr j).2.2,
le_trans_aux (fun {i} => (IHyl i).2.2) fun {j} => (IHxr j).1,
le_trans_aux (fun {i} => (IHzl i).1) fun {j} => (IHyr j).2.1⟩
lt := fun x y => x ≤ y ∧ x ⧏ y }
