exists_lt — Mathlib

English

For a decidable relation R, the function n ↦ (range s).filter (y ↦ R(y,n)) is primitive recursive.

Русский

Для разрешимого отношения R функция n ↦ (range s).filter(y ↦ R(y,n)) примитивно-рекурсивна.

LaTeX

$$$\text{Primrec}\big(n \mapsto (\mathrm{range}\, s)\;\text{filter}\; (y \mapsto \mathrm{Decidable}.decide(R(y,n)))\big).$$$

Lean4

/-- Bounded existential quantifiers are primitive recursive. -/
theorem exists_lt (hf : PrimrecPred p) : PrimrecPred fun n ↦ ∃ x < n, p x :=
  of_eq (hf.exists_mem_list.comp list_range) (by simp)

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