consRecOn_cons — Mathlib

English

If we build a word by prepending a letter to a word, consRecOn returns the step application to the rest of the word.

Русский

Если построить слово, добавив букву вперед к слову, consRecOn возвращает применение шага к остатку слова.

LaTeX

$$$\\mathrm{consRecOn}(\\mathrm{cons}\; m\; w\; h_1\\; h_2)\\; h_{empty}\\; h_{cons} = \\mathrm{consRecOn}(w)\\; h_{empty}\\; h_{cons}$$$

Lean4

@[simp]
theorem consRecOn_cons {motive : Word M → Sort*} (i) (m : M i) (w : Word M) h1 h2 (h_empty : motive empty)
    (h_cons : ∀ (i) (m : M i) (w) h1 h2, motive w → motive (cons m w h1 h2)) :
    consRecOn (cons m w h1 h2) h_empty h_cons = h_cons i m w h1 h2 (consRecOn w h_empty h_cons) :=
  rfl

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