const — Mathlib

English

For every n and every natural m, the constant function returning m is Primrec' of arity n.

Русский

Для любого n и любого натурального m константная функция, возвращающая m, является Primrec' арности n.

LaTeX

$$$$ \\forall n, \\forall m \\in \\mathbb{N}, \\; \\text{Primrec}'_n(\\lambda \\_ : \\mathrm{List.Vector}\\ \\mathbb{N}\\ n, m). $$$$

Lean4

theorem const {n} : ∀ m, @Primrec' n fun _ => m
  | 0 => zero.comp Fin.elim0 fun i => i.elim0
  | m + 1 => succ.comp _ fun _ => const m

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