alternatingWord — Mathlib

English

The function alternatingWord(i, i', m) constructs a word of length m that alternates between i and i', ending with i'.

Русский

Функция alternatingWord(i, i', m) строит слово длины m, чередующее i и i', заканчивая i'.

LaTeX

$$$\\\\text{alternatingWord}: B \\times B' \\times \\mathbb{N} \\to \\text{List}~B$ with length( alternatingWord(i, i', m) ) = m and last element i' when m>0$$

Lean4

/-- The word of length `m` that alternates between `i` and `i'`, ending with `i'`. -/
def alternatingWord (i i' : B) (m : ℕ) : List B :=
  match m with
  | 0 => []
  | m + 1 => (alternatingWord i' i m).concat i'

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