toPGame_le — Mathlib

English

If a ≤ b as ordinals, then a.toPGame ≤ b.toPGame in the PGame preorder.

Русский

Если a ≤ b как ординалы, то a.toPGame ≤ b.toPGame в порядке PGame.

LaTeX

$$$a \\le b \\Rightarrow a.toPGame \\le b.toPGame.$$$

Lean4

theorem toPGame_le {a b : Ordinal} (h : a ≤ b) : a.toPGame ≤ b.toPGame :=
  by
  refine le_iff_forall_lf.2 ⟨fun i => ?_, isEmptyElim⟩
  rw [toPGame_moveLeft']
  exact toPGame_lf ((toLeftMovesToPGame_symm_lt i).trans_le h)

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