fin_succ

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primrec.fin_succ

English

For every n, the successor map Fin(n) → Fin(n+1) is primitive recursive.

Русский

Для каждого n отображение перехода Fin(n) в Fin(n+1) является примитивно-рекурсивным.

LaTeX

$$$$ \\forall n, \\ \\operatorname{Primrec}\\big( \\mathrm{Fin.succ}(n) : \\mathrm{Fin}(n) \\to \\mathrm{Fin}(n+1) \\big). $$$$

Lean4

theorem fin_succ {n} : Primrec (@Fin.succ n) :=
  fin_val_iff.1 <| by simp [succ.comp fin_val]

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

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

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru