dest_mk — Mathlib

English

Destructing then constructing returns the original shape: dest (mk x) = x for any x in F (α ::: Cofix F α).

Русский

Разбор и конструктор возвращают исходную форму: dest (mk x) = x.

LaTeX

$$$\\forall x:\\, F(\\alpha\\append1 (\\mathrm{Cofix}\\,F\\,\\alpha)), \\; \\mathrm{dest}(\\mathrm{Cofix.mk}\\ x) = x$$$

Lean4

theorem dest_mk {α : TypeVec n} (x : F (α.append1 <| Cofix F α)) : Cofix.dest (Cofix.mk x) = x :=
  by
  have : Cofix.mk ∘ Cofix.dest = @_root_.id (Cofix F α) := funext Cofix.mk_dest
  rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp, appendFun_id_id,
    MvFunctor.id_map]

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