toPGame_nonneg — Mathlib

English

Let a be any ordinal. The associated P-game a.toPGame is nonnegative in the standard game order: 0 ≤ a.toPGame.

Русский

Пусть a — произвольный ординал. Соответствующая ему P-игра a.toPGame неотрицательна в обычном порядке игр: 0 ≤ a.toPGame.

LaTeX

$$$\forall a:\, \mathrm{Ordinal},\ 0 \le \mathrm{toPGame}(a).$$$

Lean4

theorem toPGame_nonneg (a : Ordinal) : 0 ≤ a.toPGame :=
  zeroToPGameRelabelling.ge.trans <| toPGame_le <| Ordinal.zero_le a

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