toGame_le_iff

Mathlib.SetTheory.Game.Ordinal

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

English

For ordinals a,b, a.toPGame ≈ b.toPGame iff a = b.

Русский

Для ординалов a,b выполняется a.toPGame ≈ b.toPGame тогда и только тогда, когда a = b.

LaTeX

$$(a.toPGame ≈ b.toPGame) \iff a = b$$

Lean4

theorem toGame_le_iff {a b : Ordinal} : a.toGame ≤ b.toGame ↔ a ≤ b :=
  toPGame_le_iff

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

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

Разделы

Аффилиация

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