toPGame_lt

Mathlib.SetTheory.Game.Ordinal

URI: https://scilib.ai/kg/mathlib#Ordinal.toPGame_lt

English

If a < b for ordinals, then a.toPGame < b.toPGame in the PGame order.

Русский

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

LaTeX

$$$a < b \\Rightarrow a.toPGame < b.toPGame.$$$

Lean4

theorem toPGame_lt {a b : Ordinal} (h : a < b) : a.toPGame < b.toPGame :=
  ⟨toPGame_le h.le, toPGame_lf h⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru