casesOn1 — Mathlib

English

If f is primitive recursive, then the function Nat.casesOn x m f is primitive recursive for a fixed m.

Русский

Для фиксированного m функция Nat.casesOn x m f примитивно-рекурсивна, если f примитивно-рекурсивна.

LaTeX

$$$$\\text{Nat.Primrec}(\\text{Nat.casesOn }·\\, m \\, f).$$$$

Lean4

theorem casesOn1 {f} (m : ℕ) (hf : Nat.Primrec f) : Nat.Primrec (Nat.casesOn · m f) :=
  (prec1 m (hf.comp left)).of_eq <| by simp

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