succ_nadd

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#Ordinal.succ_nadd

English

succ a ♯ b = succ (a ♯ b).

Русский

succ a ♯ b = succ (a ♯ b).

LaTeX

$$$\operatorname{succ} a \# b = \operatorname{succ}(a \# b)$$$

Lean4

theorem succ_nadd : succ a ♯ b = succ (a ♯ b) := by rw [← one_nadd (a ♯ b), ← nadd_assoc, one_nadd]

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

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

Разделы

Аффилиация

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