English
If p is a decidable predicate and hp is primitive recursive, then the projection Subtype.val is primitive recursive.
Русский
Если p — разрешимый предикат, и hp примитивно-рекурсивно, то проекция Subtype.val примитивно-рекурсивна.
LaTeX
$$$\mathrm{PR}(\text{Subtype.val})\quad\text{under } hp$, i.e. the map $x \mapsto x.1$ on $\{x: \alpha \mid p(x)\}$ is PR.$$
Lean4
/-- If `R a b` is decidable, then given `L : List α` and `b : β`, `g L b ↔ ∀ a L, R a b`
is a primitive recursive relation. -/
theorem forall_mem_list (hf : PrimrecRel R) : PrimrecRel fun (L : List α) b ↦ ∀ a ∈ L, R a b := by
classical
have h (L) (b) : (List.filter (R · b) L).length = L.length ↔ ∀ a ∈ L, R a b := by simp
apply PrimrecRel.of_eq ?_ h
exact (Primrec.eq.comp (list_length.comp <| PrimrecRel.listFilter hf) (.comp list_length fst))
