nat_sub

Mathlib.Computability.Primrec

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

English

The subtraction on natural numbers is a Primrec₂ function.

Русский

Вычитание натуральных чисел является Primrec₂.

LaTeX

$$$ Primrec_2 (fun x y => x - y) $$$

Lean4

theorem nat_sub : Primrec₂ ((· - ·) : ℕ → ℕ → ℕ) :=
  Primrec₂.unpaired'.1 Nat.Primrec.sub

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

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

Разделы

Аффилиация

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