isEmpty_powHalf_zero_rightMoves

Mathlib.SetTheory.Surreal.Dyadic

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

English

The right moves of powHalf(0) form an empty set.

Русский

Правая часть powHalf(0) пуста.

LaTeX

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

Lean4

instance isEmpty_powHalf_zero_rightMoves : IsEmpty (powHalf 0).RightMoves :=
  inferInstanceAs (IsEmpty PEmpty)

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

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

Разделы

Аффилиация

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