Ordinals

DefinitionOrdinal#

Ordinal.{u} is the type of well orders in Type u, up to order isomorphism.

Ordinal.{u} : Type (u + 1)

Sources

• Mathlib documentation: Ordinal
• Source of Ordinal in Mathlib/SetTheory/Ordinal/Basic.lean
• Mathlib overview: Logic and computation › Set theory › Ordinals

MathlibOrdinal

Used by 8

Used byLöwenheim-Skolem · Aleph numbers · Beth numbers · Cantor normal form · Epsilon numbers · Fundamental sequences · Gamma numbers · Besicovitch covering theorem

DefinitionCantor normal form#

The Cantor normal form of an ordinal o is the list of coefficients and exponents in the base-b expansion of o.

We special-case CNF 0 o = CNF 1 o = [(0, o)] for o ≠ 0.

CNF b (b ^ u₁ * v₁ + b ^ u₂ * v₂) = [(u₁, v₁), (u₂, v₂)]

Ordinal.CNF.{u_1} (b o : Ordinal.{u_1}) : List (Ordinal.{u_1} × Ordinal.{u_1})

Sources

• Mathlib documentation: Ordinal.CNF
• Source of Ordinal.CNF in Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
• Mathlib overview: Logic and computation › Set theory › Ordinals

MathlibOrdinal.CNF

Uses 3

Statement usesList · Natural number · Ordinal

StructureFundamental sequences#

A fundamental sequence for o is a strictly monotonic function Iio o.cof.ord → Iio o with cofinal range. We provide a = o.cof.ord explicitly to avoid type rewrites.

Ordinal.IsFundamentalSeq.{u_1} {a o : Ordinal.{u_1}} (f : ↑(Set.Iio a) → ↑(Set.Iio o)) : Prop

Sources

• Mathlib documentation: Ordinal.IsFundamentalSeq
• Source of Ordinal.IsFundamentalSeq in Mathlib/SetTheory/Ordinal/FundamentalSequence.lean
• Mathlib overview: Logic and computation › Set theory › Ordinals

MathlibOrdinal.IsFundamentalSeq

Uses 2

Statement usesCofinality · Ordinal

AbbreviationEpsilon numbers#

The epsilon function enumerates the fixed points of ω ^ ⬝. This is an abbreviation for veblen 1.

Conventions for notations in identifiers:

• The recommended spelling of ε_ in identifiers is epsilon.

Ordinal.epsilon.{u_1} : Ordinal.{u_1} → Ordinal.{u_1}

Sources

• Mathlib documentation: Ordinal.epsilon
• Source of Ordinal.epsilon in Mathlib/SetTheory/Ordinal/Veblen.lean
• Mathlib overview: Logic and computation › Set theory › Ordinals

MathlibOrdinal.epsilon

Uses 3

Statement usesList · Natural number · Ordinal

DefinitionGamma numbers#

The gamma function enumerates the fixed points of veblen · 0.

Of particular importance is Γ₀ = gamma 0, the Feferman-Schütte ordinal.

Conventions for notations in identifiers:

• The recommended spelling of Γ_ in identifiers is gamma.

Ordinal.gamma.{u_1} : Ordinal.{u_1} → Ordinal.{u_1}

Sources

• Mathlib documentation: Ordinal.gamma
• Source of Ordinal.gamma in Mathlib/SetTheory/Ordinal/Veblen.lean
• Mathlib overview: Logic and computation › Set theory › Ordinals

MathlibOrdinal.gamma

Uses 3

Statement usesList · Natural number · Ordinal

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.