nat_iff' — Mathlib

English

For every f : α → β → σ, Primrec₂ f is equivalent to Primrec₂ of the decoding-encoded form without pairing, i.e., a direct natural-number encoding of the inputs.

Русский

Для любой f : α → β → σ, Primrec₂ f эквивалентно Primrec₂ функции кодирования через декодирование без явной пары входов.

LaTeX

$$$ Primrec_2 f \iff Primrec_2 (\\lambda m n : \mathbb{N}. (decode α m).bind (\\lambda a. Option.map (f a) (decode β n)))$$$

Lean4

theorem nat_iff' {f : α → β → σ} :
    Primrec₂ f ↔ Primrec₂ fun m n : ℕ => (@decode α _ m).bind fun a => Option.map (f a) (@decode β _ n) :=
  nat_iff.trans <| unpaired'.trans encode_iff

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