ofFnRec_ofFn — Mathlib

English

For any h, and any f: Fin n → α, ofFnRec h (List.ofFn f) = h n f.

Русский

Для любого h и f: Fin n → α, ofFnRec h (List.ofFn f) = h n f.

LaTeX

$$$ \\operatorname{ofFnRec}\\;h\\; (\\operatorname{List.ofFn} f) = h(n)(f) $$$

Lean4

@[simp]
theorem ofFnRec_ofFn {C : List α → Sort*} (h : ∀ (n) (f : Fin n → α), C (List.ofFn f)) {n : ℕ} (f : Fin n → α) :
    @ofFnRec _ C h (List.ofFn f) = h _ f :=
  equivSigmaTuple.rightInverse_symm.cast_eq (fun s => h s.1 s.2) ⟨n, f⟩

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