instInhabitedCofixOfAP — Mathlib

English

Re-statement of corecF equality linking M.dest and appendFun with repr(g x).

Русский

Повторное утверждение равенства corecF, связывающее M.dest и appendFun с repr(g x).

LaTeX

$$$$ M.dest_{P}(\\mathrm{corecF}\\; g\\; x) = \\mathrm{appendFun}\\; \\mathrm{id}\\; (\\mathrm{corecF}\\; g) \\, \\mathrm{<$$>} \\, \\mathrm{repr}(g\\, x). $$$$

Lean4

instance {α : TypeVec n} [Inhabited q.P.A] [∀ i : Fin2 n, Inhabited (α i)] : Inhabited (Cofix F α) :=
  ⟨Quot.mk _ default⟩

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