If r is a relation on α and s in a relation on β, then f : r ≼i s is an order embedding whose range is an initial segment. That is, whenever b < f a in β then b is in the range of f.

An order isomorphism is an initial segment

The identity function shows that ≼i is reflexive

Composition of functions shows that ≼i is transitive

If we have order embeddings between α and β whose images are initial segments, and β is a well-order then α and β are order-isomorphic.

Restrict the codomain of an initial segment

Any element of a well order yields a principal segment

Restrict the codomain of a principal segment

Construct an initial segment from an order embedding.

An embedding of any type to the set of cardinals.

The relation whose existence is given by the well-ordering theorem

ordinal.{u} is the type of well orders in Type u, quotient by order isomorphism.

The order type of a well order is an ordinal.

The order type of an element inside a well order.

Ordinal less-equal is defined such that well orders r and s satisfy type r ≤ type s if there exists a function embedding r as an initial segment of s.

Ordinal less-than is defined such that well orders r and s satisfy type r < type s if there exists a function embedding r as a principal segment of s.

enum r o h is the o-th element of α ordered by r. That is, enum maps an initial segment of the ordinals, those less than the order type of r, to the elements of α.

The cardinal of an ordinal is the cardinal of any set with that order type.

The ordinal successor is the smallest ordinal larger than o. It is defined as o + 1.

The universe lift operation for ordinals, which embeds ordinal.{u} as a proper initial segment of ordinal.{v} for v > u.

ω is the first infinite ordinal, defined as the order type of ℕ.

The ordinal predecessor of o is o' if o = succ o', and o otherwise.

A limit ordinal is an ordinal which is not zero and not a successor.

A normal ordinal function is a strictly increasing function which is order-continuous.

The minimal element of a nonempty family of ordinals

The minimal element of a nonempty set of ordinals

univ.{u v} is the order type of the ordinals of Type u as a member of ordinal.{v} (when u < v). It is an inaccessible cardinal.

a - b is the unique ordinal satisfying b + (a - b) = a when b ≤ a.

a / b is the unique ordinal o satisfying a = b * o + o' with o' < b.

Divisibility is defined by right multiplication: a ∣ b if there exists c such that b = a * c.

a % b is the unique ordinal o' satisfying a = b * o + o' with o' < b.

The ordinal corresponding to a cardinal c is the least ordinal whose cardinal is c.

The cardinal univ is the cardinality of ordinal univ, or equivalently the cardinal of ordinal.{u}, or cardinal.{u}, as an element of cardinal.{v} (when u < v).

The supremum of a family of ordinals

The supremum of a family of ordinals indexed by the set of ordinals less than some o : ordinal.{u}. (This is not a special case of sup over the subtype, because {a // a < o} : Type (u+1) and sup only works over families in Type u.)

The ordinal exponential, defined by transfinite recursion.

The ordinal logarithm is the solution u to the equation x = b ^ u * v + w where v < b and w < b.

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

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

The next fixed point function, the least fixed point of the normal function f above a.

The derivative of a normal function f is the sequence of fixed points of f.

The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So aleph_idx n = n, aleph_idx ω = ω, aleph_idx ℵ₁ = ω + 1 and so on.)

The aleph' function gives the cardinals listed by their ordinal index, and is the inverse of aleph_idx. aleph' n = n, aleph' ω = ω, `aleph' (ω + 1) = ℵ₁, etc.

aleph' and aleph_idx form an equivalence between ordinal and cardinal

The aleph function gives the infinite cardinals listed by their ordinal index. aleph 0 = ω, aleph 1 = succ ω is the first uncountable cardinal, and so on.