forall_lt — Mathlib

English

If R is decidable, then the relation (n,y) ↦ ∃ x < n, R(x,y) is primitive recursive.

Русский

Если R разрешимо, то отношение (n,y) ↦ ∃ x < n, R(x,y) является примитивно-рекурсивным.

LaTeX

$$$\mathrm{PR}_2\big( (n,y) \mapsto \exists x < n\, R(x,y) \big).$$$

Lean4

/-- Bounded universal quantifiers are primitive recursive. -/
theorem forall_lt (hf : PrimrecPred p) : PrimrecPred fun n ↦ ∀ x < n, p x :=
  of_eq (hf.forall_mem_list.comp list_range) (by simp)

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