recF_eq — Mathlib

English

A standard equation for recF on a wMk element expresses its value via g and the abs/splitFun structure.

Русский

Стандартное равенство для recF на элементе wMk выражает его значение через g и структуру abs/splitFun.

LaTeX

$$$recF(g)((q.P F).wMk\; a\; f') = g(\mathrm{abs}\langle a, \mathrm{splitFun}(f', rec)\rangle).$$$

Lean4

theorem recF_eq {α : TypeVec n} {β : Type u} (g : F (α.append1 β) → β) (a : q.P.A) (f' : q.P.drop.B a ⟹ α)
    (f : q.P.last.B a → q.P.W α) : recF g (q.P.wMk a f' f) = g (abs ⟨a, splitFun f' (recF g ∘ f)⟩) := by
  rw [recF, MvPFunctor.wRec_eq]; rfl

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