comp — Mathlib

English

If f is computable and g is computable, then the composition a ↦ f(g(a)) is computable.

Русский

Если f вычислима, а g вычислима, то их композиция a ↦ f(g(a)) вычислима.

LaTeX

$$$\forall f,g:\text{type},\; Computable(f) \land Computable(g) \rightarrow Computable(\lambda a. f(g(a))).$$

Lean4

nonrec theorem comp {f : β → σ} {g : α → β} (hf : Computable f) (hg : Computable g) : Computable fun a => f (g a) :=
  hf.comp hg

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