comp₂ — Mathlib

English

If f is Primrec₂, g,h are Primrec₂, then the composition a,b ↦ f(g(a,b), h(a,b)) is Primrec₂.

Русский

Если f — Primrec₂, а g,h — Primrec₂, то композиция a,b ↦ f(g(a,b), h(a,b)) также Primrec₂.

LaTeX

$$$\operatorname{Primrec}_2 f \to \operatorname{Primrec}_2 g \to \operatorname{Primrec}_2 h \to \operatorname{Primrec}_2 (a,b \mapsto f(g(a,b), h(a,b)))$$$

Lean4

theorem comp₂ {f : γ → δ → σ} {g : α → β → γ} {h : α → β → δ} (hf : Primrec₂ f) (hg : Primrec₂ g) (hh : Primrec₂ h) :
    Primrec₂ fun a b => f (g a b) (h a b) :=
  hf.comp hg hh

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