zero_or_succ_or_isSuccLimit

Mathlib.SetTheory.Ordinal.Arithmetic

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

← MathLib Explorer

English

The value of a limit-recursion at 0 is the base case: limitRecOn 0 H1 H2 H3 = H1.

Русский

Значение ограниченной рекурсии в нуль равно базовому случаю: limitRecOn 0 H1 H2 H3 = H1.

LaTeX

$$$\mathrm{limitRecOn}(0) = H_1$$$

Lean4

theorem zero_or_succ_or_isSuccLimit (o : Ordinal) : o = 0 ∨ o ∈ range succ ∨ IsSuccLimit o := by
  simpa using isMin_or_mem_range_succ_or_isSuccLimit o

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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