one_lt_of_isSuccLimit

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

Every ordinal is either zero, a successor, or a succ-limit.

Русский

Каждый ординал либо ноль, либо следующее, либо предел суктора.

LaTeX

$$$\forall o, o = 0 \lor o \in \mathrm{range}(\mathrm{succ}) \lor \mathrm{IsSuccLimit}(o)$$$

Lean4

theorem one_lt_of_isSuccLimit {o : Ordinal} (h : IsSuccLimit o) : 1 < o :=
  mod_cast natCast_lt_of_isSuccLimit h 1

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

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

Разделы

Аффилиация

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