getElem_alternatingWord — Mathlib

English

The k-th element of the alternatingWord(i, j, p) is i if p+k is even, otherwise j (for k < p).

Русский

k-ый элемент alternatingWord(i, j, p) равен i, если p+k четно, иначе j (при k < p).

LaTeX

$$$\\\\left( alternatingWord(i, j, p) \\\\right)[k] = (if\\\\ Even(p+k) \\\\text{then } i \\\\text{else } j)$$$

Lean4

theorem getElem_alternatingWord (i j : B) (p k : ℕ) (hk : k < p) :
    (alternatingWord i j p)[k]'(by simp [hk]) = (if Even (p + k) then i else j) :=
  by
  revert k
  induction p with
  | zero => grind [not_lt_zero']
  | succ n h => grind [CoxeterSystem.alternatingWord_succ']

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