English
There are countably many partial recursive partial functions f : ℕ →. ℕ; i.e., the set { f : ℕ →. ℕ // Partrec f } is countable.
Русский
Существует счётное множество частично рекурсивных частичных функций f: ℕ →. ℕ; то есть множество { f : ℕ →. ℕ // Partrec f } счётно.
LaTeX
$$$\\mathrm{Countable}\\ { f : \\mathbb{N} \\to. \\mathbb{N} \\;//\\; \\mathrm{Partrec}\\ f }$$$
Lean4
/-- There are only countably many partial recursive partial functions `ℕ →. ℕ`. -/
instance : Countable { f : ℕ →. ℕ // _root_.Partrec f } :=
by
apply Function.Surjective.countable (f := fun c => ⟨eval c, eval_part.comp (.const c) .id⟩)
intro ⟨f, hf⟩; simpa using exists_code.1 hf