idv

Mathlib.Computability.Halting

URI: https://scilib.ai/kg/mathlib#Nat.Partrec'.idv

English

The identity vector function exists as Partrec' for every n: there is a Vec instance returning id for the n-vector.

Русский

Существует единичная (идентичная) векторная функция, являющаяся Partrec' для каждого n.

LaTeX

$$$$\forall n, \mathrm{Nat.Partrec'.Vec}(\mathrm{id}_{\mathrm{List.Vector}}).$$$$

Lean4

theorem idv {n} : @Vec n n id :=
  Vec.prim Nat.Primrec'.idv

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

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

Разделы

Аффилиация

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