const' — Mathlib

English

If s is a fixed partial value, its constant function is partial recursive (under a decidability assumption).

Русский

Постоянная функция, возвращающая фиксированное частичное значение s, частично рекурсивна при наличии допускаемой доменной decidability.

LaTeX

$$$\forall s:\Part\sigma\,[Decidable s.Dom], Partrec(\lambda _:\alpha. s).$$

Lean4

theorem _root_.Decidable.Partrec.const' (s : Part σ) [Decidable s.Dom] : Partrec fun _ : α => s :=
  (Computable.ofOption (const (toOption s))).of_eq fun _ => of_toOption s

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