map — Mathlib

English

If f is partial recursive and g is computable, then the mapped function a ↦ (f a).map (g a) is partial recursive.

Русский

Если f частично рекурсивна и g вычислима, то функция a ↦ (f a).map (g a) частично рекурсивна.

LaTeX

$$$\forall f:\alpha\to^.\beta,\; \forall g:\alpha\to\beta\to.\sigma,\ Partrec(f)\land Computable_2(g)\Rightarrow Partrec(\lambda a. (f(a)).map (g(a))).$$

Lean4

theorem map {f : α →. β} {g : α → β → σ} (hf : Partrec f) (hg : Computable₂ g) : Partrec fun a => (f a).map (g a) := by
  simpa [bind_some_eq_map] using Partrec.bind (g := fun a x => some (g a x)) hf hg

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