recF_eq' — Mathlib

English

A more explicit form: recF g x = g (abs (appendFun id (recF g) <$$> q.P.wDest' x)).

Русский

Более явная форма: recF g x = g (abs (appendFun id (recF g) <$$> q.P.wDest' x)).

LaTeX

$$$recF(g)\,x = g\bigl(\operatorname{abs}\bigl(\operatorname{appendFun} (\operatorname{id}) (recF\,g) \langle \cdot , \operatorname{wDest}'(x)\rangle\bigr)\bigr).$$$

Lean4

theorem recF_eq' {α : TypeVec n} {β : Type u} (g : F (α.append1 β) → β) (x : q.P.W α) :
    recF g x = g (abs (appendFun id (recF g) <$$> q.P.wDest' x)) :=
  by
  apply q.P.w_cases _ x
  intro a f' f
  rw [recF_eq, q.P.wDest'_wMk, MvPFunctor.map_eq, appendFun_comp_splitFun, TypeVec.id_comp]

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