casesOn' — Mathlib

English

A refinement of casesOn expressing a unpaired pairing of arguments remains primitive recursive.

Русский

Уточнение casesOn о неразделённой паре аргументов сохраняет примитивную рекурсию.

LaTeX

$$$$\\text{Nat.Primrec}(Nat.unpaired(\\lambda z,n.\\text{Nat.casesOn } n (f z) (\\lambda y. g (\\text{Nat.pair } z y))))$$$$

Lean4

theorem casesOn' {f g} (hf : Nat.Primrec f) (hg : Nat.Primrec g) :
    Nat.Primrec (unpaired fun z n => n.casesOn (f z) fun y => g <| Nat.pair z y) :=
  (prec hf (hg.comp (pair left (left.comp right)))).of_eq fun n => by simp

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