exists_mem_list — Mathlib

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 \forall a \in L\, R(a,b) \big).$$$

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 exists_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 ≠ 0 ↔ ∃ a ∈ L, R a b := by simp
  refine .of_eq (.not ?_) h
  exact Primrec.eq.comp (list_length.comp hf.listFilter) (const 0)

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