Theorems · Inductive type · logic and foundations

ONote.NF

ONote → Prop

A normal form ordinal notation has the form ω ^ a₁ * n₁ + ω ^ a₂ * n₂ + ⋯ + ω ^ aₖ * nₖ where a₁ > a₂ > ⋯ > aₖ and all the aᵢ are also in normal form. We will essentially only be interested in normal form ordinal notations, but to avoid complicating the algorithms, we define everything over general ordinal notations and only prove correctness with normal form as an invariant.

Defined in

Mathlib.SetTheory.Ordinal.Notation

Cited by

36 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms