Ordinal arithmetic
Ordinals have an addition (corresponding to disjoint union) that turns them into an additive monoid, and a multiplication (corresponding to the lexicographic order on the product) that turns them into a monoid. One can also define correspondingly a subtraction, a division, a successor function, a power function and a logarithm function.
We also define limit ordinals and prove the basic induction principle on ordinals separating
successor ordinals and limit ordinals, in limit_rec_on.
Main definitions and results
o₁ + o₂is the order on the disjoint union ofo₁ando₂obtained by declaring that every element ofo₁is smaller than every element ofo₂.o₁ - o₂is the unique ordinalosuch thato₂ + o = o₁, wheno₂ ≤ o₁.o₁ * o₂is the lexicographic order ono₂ × o₁.o₁ / o₂is the ordinalosuch thato₁ = o₂ * o + o'witho' < o₂. We also define the divisibility predicate, and a modulo operation.succ o = o + 1is the successor ofo.pred oif the predecessor ofo. Ifois not a successor, we setpred o = o.
We also define the power function and the logarithm function on ordinals, and discuss the properties
of casts of natural numbers of and of omega with respect to these operations.
Some properties of the operations are also used to discuss general tools on ordinals:
is_limit o: an ordinal is a limit ordinal if it is neither0nor a successor.limit_rec_onis the main induction principle of ordinals: if one can prove a property by induction at successor ordinals and at limit ordinals, then it holds for all ordinals.is_normal: a functionf : ordinal → ordinalsatisfiesis_normalif it is strictly increasing and order-continuous, i.e., the imagef oof a limit ordinalois the sup off afora < o.nfp f a: the next fixed point of a functionfon ordinals, abovea. It behaves well for normal functions.CNF b ois the Cantor normal form of the ordinaloin baseb.sup: the supremum of an indexed family of ordinals inType u, as an ordinal inType u.bsup: the supremum of a set of ordinals indexed by ordinals less than a given ordinalo.
Further properties of addition on ordinals
The zero ordinal
The predecessor of an ordinal
Limit ordinals
Main induction principle of ordinals: if one can prove a property by induction at successor ordinals and at limit ordinals, then it holds for all ordinals.
Equations
- o.limit_rec_on H₁ H₂ H₃ = ordinal.wf.fix (λ (o : ordinal) (IH : Π (y : ordinal), y < o → C y), dite (o = 0) (λ (o0 : o = 0), _.mpr H₁) (λ (o0 : ¬o = 0), dite (∃ (a : ordinal), o = a.succ) (λ (h : ∃ (a : ordinal), o = a.succ), _.mpr (H₂ o.pred (IH o.pred _))) (λ (h : ¬∃ (a : ordinal), o = a.succ), H₃ o _ IH))) o
Normal ordinal functions
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.
Subtraction on ordinals
Equations
Multiplication of ordinals
The multiplication of ordinals o₁ and o₂ is the (well founded) lexicographic order on
o₂ × o₁.
Equations
- ordinal.monoid = {mul := λ (a b : ordinal), quotient.lift_on₂ a b (λ (_x : Well_order), ordinal.monoid._match_2 _x) ordinal.monoid._proof_1, mul_assoc := ordinal.monoid._proof_2, one := 1, one_mul := ordinal.monoid._proof_3, mul_one := ordinal.monoid._proof_4}
- ordinal.monoid._match_2 {α := α, r := r, wo := wo} = λ (_x : Well_order), ordinal.monoid._match_1 α r wo _x
- ordinal.monoid._match_1 α r wo {α := β, r := s, wo := wo'} = ⟦{α := β × α, r := prod.lex s r, wo := _}⟧
Division on ordinals
Equations
Supremum of a family of ordinals
The supremum of a family of ordinals
Equations
- ordinal.sup f = ordinal.omin {c : ordinal | ∀ (i : ι), f i ≤ c} _
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.)
Ordinal exponential
Equations
Ordinal logarithm
The Cantor normal form
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₂)]
Equations
- ordinal.CNF b o = dite (b = 0) (λ (b0 : b = 0), list.nil) (λ (b0 : ¬b = 0), ordinal.CNF_rec b0 list.nil (λ (o : ordinal) (o0 : o ≠ 0) (h : o % b ^ ordinal.log b o < o) (IH : list (ordinal × ordinal)), (ordinal.log b o, o / b ^ ordinal.log b o) :: IH) o)
Casting naturals into ordinals, compatibility with operations
Properties of omega
Fixed points of normal functions
The next fixed point function, the least fixed point of the
normal function f above a.
Equations
- ordinal.nfp f a = ordinal.sup (λ (n : ℕ), f^[n] a)
The derivative of a normal function f is
the sequence of fixed points of f.
Equations
- ordinal.deriv f o = o.limit_rec_on (ordinal.nfp f 0) (λ (a IH : ordinal), ordinal.nfp f IH.succ) (λ (a : ordinal) (l : a.is_limit), a.bsup)