toPGame_inj

Mathlib.SetTheory.Game.Ordinal

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

English

Equality of toPGame images implies equality of ordinals: a.toPGame = b.toPGame iff a = b.

Русский

Неравенство равенству a.toPGame = b.toPGame эквивалентно a = b.

LaTeX

$$a.toPGame = b.toPGame \iff a = b$$

Lean4

@[simp]
theorem toPGame_inj {a b : Ordinal} : a.toPGame = b.toPGame ↔ a = b :=
  toPGame_injective.eq_iff

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

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

Разделы

Аффилиация

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