consRecOn_empty — Mathlib

English

Applying consRecOn to the empty word with its base case yields the base value.

Русский

Применение consRecOn к пустому слову с базовым случаем даёт базовое значение.

LaTeX

$$$\\text{consRecOn empty h_{empty} h_{cons}} = h_{empty}$$$

Lean4

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

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