isEmpty_zero_toPGame_leftMoves

Mathlib.SetTheory.Game.Ordinal

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

English

The left moves of the zero ordinal’s p-game are empty.

Русский

Левые ходы нулевой ординали в PGame пусты.

LaTeX

$$$IsEmpty((toPGame 0).LeftMoves).$$$

Lean4

instance isEmpty_zero_toPGame_leftMoves : IsEmpty (toPGame 0).LeftMoves := by rw [toPGame_leftMoves]; infer_instance

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

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

Разделы

Аффилиация

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