option_some_iff — Mathlib

English

For any f: α → σ, the statement (Primrec (λ a, Some (f a))) holds iff Primrec f.

Русский

Для любого f: α → σ, Primrec (λ a, Some (f a)) эквивалентно Primrec f.

LaTeX

$$$$ (\\mathrm{Primrec}\\bigl(\\lambda a. \\mathrm{Some}(f(a))\\bigr)) \\iff \\mathrm{Primrec}(f) $$$$

Lean4

theorem option_some_iff {f : α → σ} : (Primrec fun a => some (f a)) ↔ Primrec f :=
  ⟨fun h => encode_iff.1 <| pred.comp <| encode_iff.2 h, option_some.comp⟩

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