English
If f: α → β, p a predicate, and h(a) ensures p holds, then f is computable as a function into the subtype defined by p, provided PrimrecPred p and hf computable.
Русский
Если f: α → β, задано p: β → Prop и gens обеспечивают выполнение p, то f можно считать вычислимым как функцию в подтипе p, при условии PrimrecPred p и вычислимости hf.
LaTeX
$$$\forall f:\alpha \to \beta\,\, p:\beta\to\mathrm{Prop},\; (\mathrm{DecidablePred } p) \Rightarrow \mathrm{Computable} f \Rightarrow \mathrm{Computable} (\lambda a. (⟨f a, h a⟩ : Subtype p))$$$
Lean4
theorem subtype_mk {f : α → β} {p : β → Prop} [DecidablePred p] {h : ∀ a, p (f a)} (hp : PrimrecPred p)
(hf : Computable f) : @Computable _ _ _ (Primcodable.subtype hp) fun a => (⟨f a, h a⟩ : Subtype p) :=
hf
