const — Mathlib

English

For every natural number n, the constant function returning n is primitive recursive, built inductively starting from zero.

Русский

Для каждого числа n константная функция, возвращающая n, примитивно-рекурсивна; базируется на нуле и последующем шаге.

LaTeX

$$$$\\text{const}(n) : \\text{Nat.Primrec}(\\lambda k => n).$$$$

Lean4

theorem const : ∀ n : ℕ, Nat.Primrec fun _ => n
  | 0 => zero
  | n + 1 => Primrec.succ.comp (const n)

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