corec — Mathlib

English

Corecursor for Cofix F: given g : β → F (α ::: β), there is a canonical way to produce an element of Cofix F α from β, denoted corec g.

Русский

Коре-курсор Cofix F: для данного g : β → F (α ::: β) существует канонический способ получить элемент Cofix F α из β, обозначаемый corec g.

LaTeX

$$$\\mathrm{corec}\\; g\\; :\\; \\beta \\to \\mathrm{Cofix}\\,F\\,\\alpha\\quad\\text{with}\\quad \\mathrm{corec}\\; g\\; x = \\operatorname{Quot.mk}\\,\\left(\\mathrm{corecF}\\, g\\, x\\right).$$$

Lean4

/-- Corecursor for `Cofix F` -/
def corec {α : TypeVec n} {β : Type u} (g : β → F (α.append1 β)) : β → Cofix F α := fun x => Quot.mk _ (corecF g x)

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