toGame_inj

Mathlib.SetTheory.Game.Ordinal

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

English

For ordinals a,b, a.toGame = b.toGame iff a = b.

Русский

Для ординалов a,b: a.toGame = b.toGame эквивалентно a = b.

LaTeX

$$a.toGame = b.toGame \iff a = b$$

Lean4

theorem toGame_inj {a b : Ordinal} : a.toGame = b.toGame ↔ a = b :=
  toGame.inj

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

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

Разделы

Аффилиация

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