powHalf_leftMoves

Mathlib.SetTheory.Surreal.Dyadic

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

English

For every n, the set of left moves of powHalf(n) is a singleton (has exactly one element).

Русский

Для каждого n множество левых ходов powHalf(n) является единичным по размеру (один элемент).

LaTeX

$$$|\mathrm{LeftMoves}(\text{powHalf}(n))| = 1$$$

Lean4

theorem powHalf_leftMoves (n) : (powHalf n).LeftMoves = PUnit := by cases n <;> rfl

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

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

Разделы

Аффилиация

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