English
For any decidable predicate p, the relation L ↦ ∃ a ∈ L, p(a) is primitive recursive. In particular, there is a primitive-recursive predicate expressing that some element of a list satisfies p.
Русский
Для любого разрешимого предиката p отношение L ↦ ∃ a ∈ L, p(a) является примитивно-рекурсивным. В частности, существует примитивно-рекурсивное выражение существования элемента списка, удовлетворяющего p.
LaTeX
$$$\forall p\ ( ext{Decidable}(p) \Rightarrow \mathrm{PR}(L \mapsto \exists a \in L\, p(a))).$$$
Lean4
/-- Checking if any element of a list satisfies a decidable predicate is primitive recursive. -/
theorem exists_mem_list : (hf : PrimrecPred p) → PrimrecPred fun L : List α ↦ ∃ a ∈ L, p a
| ⟨_, hf⟩ => .of_eq (.not <| Primrec.eq.comp (list_length.comp <| listFilter hf.primrecPred) (const 0)) <| by simp
