ONote

Mathlib.SetTheory.Ordinal.Notation

URI: https://scilib.ai/kg/mathlib#ONote

Lean4

/-- Recursive definition of an ordinal notation. `zero` denotes the ordinal 0, and `oadd e n a` is
intended to refer to `ω ^ e * n + a`. For this to be a valid Cantor normal form, we must have the
exponents decrease to the right, but we can't state this condition until we've defined `repr`, so we
make it a separate definition `NF`. -/
inductive ONote : Type
  | zero : ONote
  | oadd : ONote → ℕ+ → ONote → ONote
  deriving DecidableEq

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

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

Разделы

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

Аффилиация

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