subtype_mk — Mathlib

English

If p is decidable and hp is primitive recursive, then the map x ↦ x.1 from {x : α | p x} to α is primitive recursive.

Русский

Если p разрешимо и hp примитивно-рекурсивно, то отображение x ↦ x.1 из подтипа {x : α | p x} в α примитивно-рекурсивно.

LaTeX

$$$\mathrm{PR}(\operatorname{Subtype}.\mathrm{val})$ under hp, i.e. the projection from the subtype is PR.$$

Lean4

theorem subtype_mk {p : β → Prop} [DecidablePred p] {hp : PrimrecPred p} {f : α → β} {h : ∀ a, p (f a)}
    (hf : Primrec f) :
    haveI := Primcodable.subtype hp
    Primrec fun a => @Subtype.mk β p (f a) (h a) :=
  subtype_val_iff.1 hf

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