dest_corec — Mathlib

English

Destructor equality for corecursion: the destination of a corec g x equals the map of g x under the appropriate cofibration.

Русский

Равенство деструктора для корекурсии: dest(corec g x) равно отображению g x через соответствующую конструирующую операцию.

LaTeX

$$$\\mathrm{dest}\\big(\\mathrm{Cofix.corec}\\ g\\ x\\big) = \\operatorname{appendFun}\\ id\\big(\\mathrm{Cofix.corec}\\ g\\big)\\; <$$>\\; g\\ x.$$$

Lean4

theorem dest_corec {α : TypeVec n} {β : Type u} (g : β → F (α.append1 β)) (x : β) :
    Cofix.dest (Cofix.corec g x) = appendFun id (Cofix.corec g) <$$> g x :=
  by
  conv =>
    lhs
    rw [Cofix.dest, Cofix.corec]
  dsimp
  rw [corecF_eq, abs_map, abs_repr, ← comp_map, ← appendFun_comp]; rfl

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