vector_toList_iff — Mathlib

English

For any n and any f : α → List.Vector β n, the Primrec property of a → (f a).toList is equivalent to Primrec f.

Русский

Пусть n задано, и f : α → List.Vector β n. Примитивно-рекурсивность функции a ↦ (f(a).toList) эквивалентна примитивно-рекурсивности самой функции f.

LaTeX

$$$$ ( \\operatorname{Primrec}( \\lambda a, (f\\,a).toList ) ) \\iff ( \\operatorname{Primrec} f ). $$$$

Lean4

theorem vector_toList_iff {n} {f : α → List.Vector β n} : (Primrec fun a => (f a).toList) ↔ Primrec f :=
  subtype_val_iff

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