option_get — Mathlib

English

If f is primitive recursive and ∀ a, p(f(a)) holds, then a ↦ ⟨f(a), h(a)⟩ is primitive recursive.

Русский

Если f примитивно-рекурсивна и для всех a выполняется p(f(a)), то a ↦ ⟨f(a), h(a)⟩ примитивно-рекурсивно.

LaTeX

$$$\mathrm{PR}(f) \rightarrow \mathrm{PR}\big(a \mapsto \langle f(a), h(a) \rangle\big).$$$

Lean4

theorem option_get {f : α → Option β} {h : ∀ a, (f a).isSome} : Primrec f → Primrec fun a => (f a).get (h a) :=
  by
  intro hf
  refine (Nat.Primrec.pred.comp hf).of_eq fun n => ?_
  generalize hx : @decode α _ n = x
  cases x <;> simp

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