nat_double

Mathlib.Computability.Primrec

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

English

Doubling is primitive recursive.

Русский

Удвоение является примитивно вычисимой функцией.

LaTeX

$$$\\text{nat\\_double}: \\mathbb{N}\\to\\mathbb{N}$ is primitive recursive.$$

Lean4

theorem nat_double : Primrec (fun n : ℕ => 2 * n) :=
  nat_mul.comp (const _) Primrec.id

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

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

Разделы

Аффилиация

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