powHalf_moveLeft

Mathlib.SetTheory.Surreal.Dyadic

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

English

For all n and for every left move index i, the left move from powHalf(n) yields 0.

Русский

Для всех n и каждого индекса левого хода i левый ход из powHalf(n) даёт 0.

LaTeX

$$$\forall n, \forall i \in \mathrm{LeftMoves}(\text{powHalf}(n)), \ (\text{powHalf}(n)).\mathrm{moveLeft}\,i = 0$$$

Lean4

@[simp]
theorem powHalf_moveLeft (n i) : (powHalf n).moveLeft i = 0 := by cases n <;> cases i <;> rfl

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

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

Разделы

Аффилиация

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