nat_lt

Mathlib.Computability.Primrec

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

English

Less-than on natural numbers is primitive recursive.

Русский

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

LaTeX

$$$\\PrimrecRel\\big((<) : \\mathbb{N} \\to \\mathbb{N} \\to \\mathrm{Prop}\\big)$$$

Lean4

theorem nat_lt : PrimrecRel ((· < ·) : ℕ → ℕ → Prop) :=
  (nat_le.comp snd fst).not.of_eq fun p => by simp

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

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

Разделы

Аффилиация

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