mk_dest — Mathlib

English

Fix.dest is inverse to Fix.mk up to quotient structure: Fix.mk x.dest equals x for all x in Fix F α.

Русский

Fix.dest обратно к Fix.mk через факторизацию: Fix.mk x.dest = x для всех x.

LaTeX

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

Lean4

theorem mk_dest (x : Fix F α) : Fix.mk (Fix.dest x) = x :=
  by
  change (Fix.mk ∘ Fix.dest) x = x
  apply Fix.ind_rec
  intro x; dsimp
  rw [Fix.dest, Fix.rec_eq, ← comp_map, ← appendFun_comp, id_comp]
  intro h; rw [h]
  change Fix.mk (appendFun id id <$$> x) = Fix.mk x
  rw [appendFun_id_id, MvFunctor.id_map]

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