nat_add

Mathlib.Computability.Primrec

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

English

The map-into-decode form is equivalent to Primrec₂ f, by using the equivalence with bind and option_some.

Русский

Эквивалентность: отображение в декодирование эквивалентно Primrec₂ f.

LaTeX

$$$ (Primrec_2 fun a n => Option.map (f a) (decode n)) \iff Primrec_2 f$$$

Lean4

theorem nat_add : Primrec₂ ((· + ·) : ℕ → ℕ → ℕ) :=
  Primrec₂.unpaired'.1 Nat.Primrec.add

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

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

Разделы

Аффилиация

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