IsNormal

Mathlib.SetTheory.Ordinal.Arithmetic

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

Lean4

/-- A normal ordinal function is a strictly increasing function which is
  order-continuous, i.e., the image `f o` of a limit ordinal `o` is the sup of `f a` for
  `a < o`.

  Todo: deprecate this in favor of `Order.IsNormal`. -/
def IsNormal (f : Ordinal → Ordinal) : Prop :=
  Order.IsNormal f

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

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

Разделы

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

Аффилиация

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