alternatingWord_succ — Mathlib

English

The word of length m+1 is obtained by appending i' to the word of length m, alternating with i and i'.

Русский

Слово длины m+1 получается добавлением i' к слову длины m, чередуясь с i и i'.

LaTeX

$$$\\\\text{alternatingWord}(i, i', m+1) = (\\\\text{alternatingWord}(i', i, m)) \\\\cdot [i']$$$

Lean4

theorem alternatingWord_succ (i i' : B) (m : ℕ) : alternatingWord i i' (m + 1) = (alternatingWord i' i m).concat i' :=
  rfl

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