none — Mathlib

English

The constant undefined partial function is partial recursive.

Русский

Постоянная частично неопределенная функция является частично вычислимой.

LaTeX

$$$\forall \alpha\sigma\,[\text{Primcodable }\alpha]\,[\text{Primcodable }\sigma]: Partrec(\lambda _:\alpha. Part.none\;\sigma).$$

Lean4

theorem none : Partrec fun _ : α => @Part.none σ :=
  Nat.Partrec.none.of_eq fun n => by cases decode (α := α) n <;> simp

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