powHalf_succ_moveRight — Mathlib

English

For every n and every right move index i, the right move from powHalf(n+1) yields powHalf(n).

Русский

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

LaTeX

$$$\forall n, \forall i \in \mathrm{RightMoves}(\text{powHalf}(n+1)), \ (\text{powHalf}(n+1)).\mathrm{moveRight}\,i = \text{powHalf}(n)$$$

Lean4

@[simp]
theorem powHalf_succ_moveRight (n i) : (powHalf (n + 1)).moveRight i = powHalf n :=
  rfl

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