forall_lt — Mathlib

English

For decidable R on naturals, the relation (n,y) ↦ ∃ x < n, R(x,y) is primitive recursive.

Русский

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

LaTeX

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

Lean4

/-- If `R a b` is decidable, then for any fixed `n` and `y`, `g n y ↔ ∀ x < n, R x y` is a
primitive recursive relation. -/
theorem forall_lt (hf : PrimrecRel R) : PrimrecRel fun n y ↦ ∀ x < n, R x y :=
  (hf.forall_mem_list.comp (list_range.comp fst) snd).of_eq (by simp)

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