English
If R is decidable, then the relation g(L,b) ↔ ∃ a ∈ L, R(a,b) is primitive recursive.
Русский
Если R разрешимо, то отношение g(L,b) ↔ ∃ a ∈ L, R(a,b) примитивно-рекурсивно.
LaTeX
$$$\mathrm{PR}\big( (L,b) \mapsto \exists a \in L\, R(a,b) \big).$$$
Lean4
/-- If `R a b` is decidable, then given `L : List α` and `b : β`, it is primitive recursive
to filter `L` for elements `a` with `R a b` -/
theorem listFilter (hf : PrimrecRel R) [DecidableRel R] : Primrec₂ fun (L : List α) b ↦ L.filter (fun a ↦ R a b) :=
by
simp only [← List.filterMap_eq_filter]
refine listFilterMap fst (Primrec.ite ?_ ?_ (Primrec.const Option.none))
· exact Primrec.eq.comp (hf.decide.comp snd (snd.comp fst)) (.const true)
· exact (option_some).comp snd
