prec1 — Mathlib

English

Given a primitive recursive f, one can build a primitive recursive function recursing with a fixed step m.

Русский

Данная к примитивно-рекурсивной f можно построить функцию рекурсивно с фиксированным шагом m.

LaTeX

$$$$\\text{prec1}(m,f) : \\text{Nat.Primrec}(n \\mapsto Nat.rec\\; m\\; (\\lambda y IH. f(\\langle y, IH \\rangle))\\; n).$$$$

Lean4

theorem prec1 {f} (m : ℕ) (hf : Nat.Primrec f) : Nat.Primrec fun n => n.rec m fun y IH => f <| Nat.pair y IH :=
  ((prec (const m) (hf.comp right)).comp (zero.pair Primrec.id)).of_eq fun n => by simp

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