option_some_iff — Mathlib

English

For any f: α → β → σ, the function (a,b) ↦ Some(f(a,b)) is primitive recursive in two arguments iff f is.

Русский

Для любой f: α → β → σ, функция (a,b) ↦ Some(f(a,b)) примитивно вычислима по двум аргументам тогда и только тогда, когда f является таковой.

LaTeX

$$$\operatorname{Primrec}_2(\lambda a,b. \text{Some}(f(a,b))) \iff \operatorname{Primrec}_2 f$$$

Lean4

theorem option_some_iff {f : α → β → σ} : (Primrec₂ fun a b => some (f a b)) ↔ Primrec₂ f :=
  Primrec.option_some_iff

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