dest_mk — Mathlib

English

A specialized equality showing that the constructor and destructor compose to the identity on the canonical level via wrepr equivalence.

Русский

Специальное равенство, показывающее что конструктор и деструктор составляют единицу на каноническом уровне через wrepr.

LaTeX

$$$\mathrm{Fix.mk} x \mathrm{dest} = x$$$

Lean4

theorem dest_mk (x : F (append1 α (Fix F α))) : Fix.dest (Fix.mk x) = x :=
  by
  unfold Fix.dest
  rw [Fix.rec_eq, ← Fix.dest, ← comp_map]
  conv =>
    rhs
    rw [← MvFunctor.id_map x]
  rw [← appendFun_comp, id_comp]
  have : Fix.mk ∘ Fix.dest (F := F) (α := α) = _root_.id :=
    by
    ext (x : Fix F α)
    apply Fix.mk_dest
  rw [this, appendFun_id_id]

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