rec_unique — Mathlib

English

Fix.rec is the unique morphism into β given a recursive definition: if g and h agree on Fix.mk x for all x, then Fix.rec g = h.

Русский

Fix.rec единственна по отношению к отображению; если два отображения совпадают на конструкторе Fix.mk, то они совпадают на всех элементах.

LaTeX

$$$\forall {g : F (\alpha.append1 \beta) \to \beta} (h : \mathrm{Fix} F \alpha \to \beta),\; (\forall x, h(\mathrm{Fix.mk} x) = g(\mathrm{appendFun} id h <$$> x)) \Rightarrow \mathrm{Fix.rec} \ g = h$$$

Lean4

theorem rec_unique {β : Type u} (g : F (append1 α β) → β) (h : Fix F α → β)
    (hyp : ∀ x, h (Fix.mk x) = g (appendFun id h <$$> x)) : Fix.rec g = h :=
  by
  ext x
  apply Fix.ind_rec
  intro x hyp'
  rw [hyp, ← hyp', Fix.rec_eq]

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