forall_mem_list — Mathlib

English

For any decidable predicate p, the relation L ↦ ∀ a ∈ L, p(a) is primitive recursive.

Русский

Для любого разрешимого предиката p отношение L ↦ ∀ a ∈ L, p(a) является примитивно-рекурсивным.

LaTeX

$$$\forall p\ (\text{Decidable}(p) \Rightarrow \mathrm{PR}(L \mapsto \forall a \in L\, p(a))).$$$

Lean4

/-- Checking if every element of a list satisfies a decidable predicate is primitive recursive. -/
theorem forall_mem_list : (hf : PrimrecPred p) → PrimrecPred fun L : List α ↦ ∀ a ∈ L, p a
  | ⟨_, hf⟩ => .of_eq (Primrec.eq.comp (list_length.comp <| listFilter hf.primrecPred) (list_length)) <| by simp

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