toPGame_leftMoves

Mathlib.SetTheory.Game.Ordinal

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

English

The left moves of the p-game corresponding to an ordinal o are in bijection with the elements of o’s type.

Русский

Левые ходы соответствующей ordinal-игры образуют биекцию с элементами типа o.

LaTeX

$$$o.toPGame.LeftMoves \\\\cong o.toType.$$$

Lean4

@[simp]
theorem toPGame_leftMoves (o : Ordinal) : o.toPGame.LeftMoves = o.toType := by rw [toPGame, LeftMoves]

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

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

Разделы

Аффилиация

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