ofNat_succ

Mathlib.SetTheory.Ordinal.Notation

URI: https://scilib.ai/kg/mathlib#ONote.ofNat_succ

English

ofNat(n+1) = oadd 0 n.succPNat 0.

Русский

ofNat(n+1) = oadd 0 n.succPNat 0.

LaTeX

$$$\operatorname{ofNat}(n+1) = \operatorname{oadd} 0 (n^{succPNat}) 0$$$

Lean4

@[simp]
theorem ofNat_succ (n) : ofNat (Nat.succ n) = oadd 0 n.succPNat 0 :=
  rfl

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

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

Разделы

Аффилиация

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