powHalf_zero_rightMoves

Mathlib.SetTheory.Surreal.Dyadic

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.powHalf_zero_rightMoves

English

powHalf(0) has no right moves; its right move set is empty.

Русский

powHalf(0) не имеет правых ходов; множество правых ходов пусто.

LaTeX

$$$(\text{powHalf}(0)).\mathrm{RightMoves} = \emptyset$$$

Lean4

theorem powHalf_zero_rightMoves : (powHalf 0).RightMoves = PEmpty :=
  rfl

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

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

Разделы

Аффилиация

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