subtype_val — Mathlib

English

If R is decidable, then the primitive recursive relation exists a in L with R(a,b) holds is expressible as g(L,b) ≡ ∃ a ∈ L, R(a,b).

Русский

Если R разрешимо, то примитивно-рекурсивно выражается существование a в L, такого что R(a,b).

LaTeX

$$$\mathrm{PR}\big( (L,b) \mapsto \exists a \in L\, R(a,b) \big).$$$

Lean4

theorem subtype_val {p : α → Prop} [DecidablePred p] {hp : PrimrecPred p} :
    haveI := Primcodable.subtype hp
    Primrec (@Subtype.val α p) :=
  by
  letI := Primcodable.subtype hp
  refine (Primcodable.prim (Subtype p)).of_eq fun n => ?_
  rcases @decode (Subtype p) _ n with (_ | ⟨a, h⟩) <;> rfl

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