nat_max

Mathlib.Computability.Primrec

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

English

The maximum of two natural numbers is a primitive recursive function.

Русский

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

LaTeX

$$$\\max:\\mathbb{N}\\times\\mathbb{N}\\to\\mathbb{N}$ is primitive recursive.$$

Lean4

theorem nat_max : Primrec₂ (@max ℕ _) :=
  ite (nat_le.comp fst snd) snd fst

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

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

Разделы

Аффилиация

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