list_map — Mathlib

English

Mapping a list by a parameter-dependent function is primitive recursive.

Русский

Отображение списка по функции, зависящей от параметра, является примитивно вычислимым.

LaTeX

$$$\\mathrm{Primrec}\\left( a \\mapsto (f(a)).\\mathrm{map}(g(a)) \\right)$$$

Lean4

theorem list_map {f : α → List β} {g : α → β → σ} (hf : Primrec f) (hg : Primrec₂ g) :
    Primrec fun a => (f a).map (g a) :=
  (list_foldr hf (const []) <| to₂ <| list_cons.comp (hg.comp fst (fst.comp snd)) (snd.comp snd)).of_eq fun a => by
    induction f a <;> simp [*]

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