dest_corec — Mathlib

English

For any corecursive construction corec g x, the outer destructor (dest) applied to this object equals the functor map of corec g applied to g x. This expresses compatibility between corecursion and destructors.

Русский

Для любой конструкции corec g x, внешний деструктор (dest), применяемый к этому объекту, равен отображению-функтором (map) от corec g по аргументу g x. Это выражает совместимость корекурсии с деструкторами.

LaTeX

$$$\forall {P,\alpha}, (g:\alpha\to P.\alpha), (x:\alpha)\;:\; M.dest( M.corec\ g\ x) = P.map( M.corec\ g)(g\ x)$$$

Lean4

theorem dest_corec (g : α → P α) (x : α) : M.dest (M.corec g x) = P.map (M.corec g) (g x) := by rw [corec_def, dest_mk]

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