nat_double_succ

Mathlib.Computability.Primrec

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

English

2n+1 is primitive recursive.

Русский

2n+1 является примитивно вычисимой функцией.

LaTeX

$$$\\text{Nat.double\\_succ}: \\mathbb{N}\\to\\mathbb{N}$ is primitive recursive.$$

Lean4

theorem nat_double_succ : Primrec (fun n : ℕ => 2 * n + 1) :=
  nat_double |> Primrec.succ.comp

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

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

Разделы

Аффилиация

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