alternatingWord_succ' — Mathlib

English

A refined description of how alternatingWord grows by one step, depending on parity.

Русский

Уточнённое описание роста alternatingWord на одну ступеньку в зависимости от чётности.

LaTeX

$$$\\\\text{alternatingWord}(i, i', m+1) = (if\\\\ Even(m) \\\\text{then } i' \\\\text{else } i) :::\\\\text{alternatingWord}(i, i', m)$$$

Lean4

theorem alternatingWord_succ' (i i' : B) (m : ℕ) :
    alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m := by
  induction m generalizing i i' with
  | zero => simp [alternatingWord]
  | succ m ih =>
    rw [alternatingWord]
    nth_rw 1 [ih i' i]
    rw [alternatingWord]
    simp [Nat.even_add_one, -Nat.not_even_iff_odd]

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