add_succ

Mathlib.SetTheory.Ordinal.Basic

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

English

Adding a successor on the right shifts the sum by one: o1 + succ(o2) = succ(o1 + o2).

Русский

При сложении справа к числу-правому добавляется единица: o1 + succ(o2) = succ(o1 + o2).

LaTeX

$$$ o_1 + \operatorname{succ}(o_2) = \operatorname{succ}(o_1 + o_2) $$$

Lean4

theorem add_succ (o₁ o₂ : Ordinal) : o₁ + succ o₂ = succ (o₁ + o₂) :=
  (add_assoc _ _ _).symm

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

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

Разделы

Аффилиация

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