const' — Mathlib

English

For any fixed partial value s, the constant function returning s is partial recursive.

Русский

Для любого фиксированного частичного значения s константная функция, возвращающая s, частично рекурсивна.

LaTeX

$$$\forall s:\Part\sigma, Partrec(\lambda _:\alpha. s).$$

Lean4

theorem const' (s : Part σ) : Partrec fun _ : α => s :=
  haveI := Classical.dec s.Dom
  Decidable.Partrec.const' s

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