corecF_eq — Mathlib

English

The destination of corecF g x equals the image of repr(g x) under the appendFun inverse structure.

Русский

Назначение corecF g x равняется образу repr(g x) под структурой appendFun.

LaTeX

$$$$ \\mathrm{dest}_{P}(\\mathrm{corecF}\\; g\\; x) = \\mathrm{appendFun}\\;\\mathrm{id}\\; (\\mathrm{corecF}\\; g)\\; \\langle\\mathrm{id}, \\mathrm{repr}(g\\, x)\\rangle. $$$$

Lean4

theorem corecF_eq {α : TypeVec n} {β : Type u} (g : β → F (α.append1 β)) (x : β) :
    M.dest q.P (corecF g x) = appendFun id (corecF g) <$$> repr (g x) := by rw [corecF, M.dest_corec]

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