finRecOn_mk — Mathlib

English

Specializing the recursion principle to a canonical representative: if q is the canonical element mk a · for some a : ∀ i, α i, then finRecOn q (C := C) equals the function that maps f to f a.

Русский

Специализация принципа рекурсии к каноническому представителю: если q есть канонический элемент mk a · для некоторого a : ∀ i, α i, тогда finRecOn q = (f ↦ f a).

LaTeX

$$$finRecOn\left(\mathrm{⟦}a\cdot\right) = (\lambda f\,\_.\, f(a))$$$

Lean4

@[simp]
theorem finRecOn_mk {C : (∀ i, Trunc (α i)) → Sort*} (a : ∀ i, α i) : finRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a :=
  by
  unfold finRecOn
  simp

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