dest_corec — Mathlib

English

The destructor of a multivariate functor corecursion coherently maps the corecursive structure to a type-level resolved form.

Русский

Деградация многофунктора в процессе ядро-рекурсии согласованно отображает структуру на разрешённую форму типа.

LaTeX

$$$\\forall {\\alpha},{\\beta},\\; M.dest\\ P\\ (M.corec\\ P\\ g\\ x) = (appendFun\\ id\\ (M.corec\\ P\\ g))\\ <$$>\\ g\\ x$$$

Lean4

theorem dest_corec {α : TypeVec n} {β : Type u} (g : β → P (α.append1 β)) (x : β) :
    M.dest P (M.corec P g x) = appendFun id (M.corec P g) <$$> g x :=
  by
  trans
  · apply M.dest_corec'
  obtain ⟨a, f⟩ := g x; dsimp
  rw [MvPFunctor.map_eq]; congr
  conv_rhs => rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]
  rfl

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