instCountableSubtypeForallComputable

English

There are countably many computable functions f : ℕ → ℕ; i.e., the set { f : ℕ → ℕ // Computable f } is countable.

Русский

Существует счётное множество вычислимых функций f : ℕ → ℕ; то есть множество { f : ℕ → ℕ // Computable f } счётно.

LaTeX

$$$\\mathrm{Countable}\\{ f : \\mathbb{N} \\to \\mathbb{N} // \\mathrm{Computable}\\ f\\}$$$

Lean4

/-- There are only countably many computable functions `ℕ → ℕ`. -/
instance : Countable { f : ℕ → ℕ // Computable f } :=
  @Function.Injective.countable { f : ℕ → ℕ // Computable f } { f : ℕ →. ℕ // _root_.Partrec f } _
    (fun f => ⟨f.val, f.2⟩) (fun _ _ h => Subtype.val_inj.1 (PFun.lift_injective (by simpa using h)))

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