isSuccLimit_add

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

If b is a successor-limit, then a + b is a successor-limit.

Русский

Если b является succ-пределом, то a + b является succ-пределом.

LaTeX

$$IsSuccLimit(b) \Rightarrow IsSuccLimit(a + b)$$

Lean4

theorem isSuccLimit_add (a : Ordinal) {b : Ordinal} : IsSuccLimit b → IsSuccLimit (a + b) :=
  (isNormal_add_right a).isSuccLimit

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

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

Разделы

Аффилиация

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