rec_unique — Mathlib

English

If g : F α → α and h : Fix F → α satisfy h (Fix.mk x) = g (h <$> x) for all x, then Fix.rec g = h.

Русский

Если g : F α → α и h : Fix F → α удовлетворяют h (Fix.mk x) = g (h <$> x) для всех x, то Fix.rec g = h.

LaTeX

$$$$\forall {F : Type u \to Type u} [q : QPF F] {\alpha : Type u} (g : F \alpha \to \alpha) (h : Fix F \to \alpha), (\forall x, h (Fix.mk x) = g (h <$> x)) \rightarrow Fix.rec g = h.$$$$

Lean4

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

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