instCountableSubtypePFunPartrec — Mathlib

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

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