comp — Mathlib

English

For functions on natural numbers, Partrec is equivalent to Nat.Partrec.

Русский

Для функций на натуральных числах Partrec эквивалентна Nat.Partrec.

LaTeX

$$$\Partrec f \iff Nat.Partrec f\,\,\text{для } f: \mathbb{N} \to^. \mathbb{N}.$$

Lean4

nonrec theorem comp {f : β →. σ} {g : α → β} (hf : Partrec f) (hg : Computable g) : Partrec fun a => f (g a) :=
  (hf.comp hg).of_eq fun n => by simp; rcases e : decode (α := α) n with - | a <;> simp [encodek]

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