corec_def — Mathlib

English

The corecursion operator M.corec satisfies a definitional unfolding: M.corec f x0 = M.mk (F.map (M.corec f) (f x0)).

Русский

Оперирование по ядру с помощью corec удовлетворяет определению развёртывания: M.corec f x0 = M.mk (F.map (M.corec f) (f x0)).

LaTeX

$$$\\operatorname{M.corec}\\ f\\ x_0 = \\operatorname{M.mk}\\big(\\operatorname{F.map}(\\operatorname{M.corec}\\ f)(f\\ x_0)\\big)$$$

Lean4

theorem corec_def {X} (f : X → F X) (x₀ : X) : M.corec f x₀ = M.mk (F.map (M.corec f) (f x₀)) :=
  by
  dsimp only [M.corec, M.mk]
  congr with n
  rcases n with - | n
  · dsimp only [sCorec, Approx.sMk]
  · dsimp only [sCorec, Approx.sMk]
    cases f x₀
    dsimp only [PFunctor.map]
    congr

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