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 limitRecOn
.
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 ordinalo
such thato₂ + o = o₁
, wheno₂ ≤ o₁
.o₁ * o₂
is the lexicographic order ono₂ × o₁
.o₁ / o₂
is the ordinalo
such thato₁ = o₂ * o + o'
witho' < o₂
. We also define the divisibility predicate, and a modulo operation.Order.succ o = o + 1
is the successor ofo
.pred o
if the predecessor ofo
. Ifo
is not a successor, we setpred o = o
.
We discuss the properties of casts of natural numbers of and of ω
with respect to these
operations.
Some properties of the operations are also used to discuss general tools on ordinals:
IsLimit o
: an ordinal is a limit ordinal if it is neither0
nor a successor.limitRecOn
is 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.IsNormal
: a functionf : Ordinal → Ordinal
satisfiesIsNormal
if it is strictly increasing and order-continuous, i.e., the imagef o
of a limit ordinalo
is the sup off a
fora < o
.sup
,lsub
: the supremum / least strict upper bound of an indexed family of ordinals inType u
, as an ordinal inType u
.bsup
,blsub
: the supremum / least strict upper bound of a set of ordinals indexed by ordinals less than a given ordinalo
.
Various other basic arithmetic results are given in Principal.lean
instead.
Further properties of addition on ordinals #
The predecessor of an ordinal #
The ordinal predecessor of o
is o'
if o = succ o'
,
and o
otherwise.
Equations
- o.pred = if h : ∃ (a : Ordinal.{?u.2}), o = Order.succ a then Classical.choose h else o
Instances For
Limit ordinals #
A limit ordinal is an ordinal which is not zero and not a successor.
TODO: deprecate this in favor of Order.IsSuccLimit
.
Equations
- o.IsLimit = Order.IsSuccLimit o
Instances For
Alias of Ordinal.IsLimit.isSuccPrelimit
.
Alias of Ordinal.isSuccPrelimit_zero
.
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.limitRecOn H₁ H₂ H₃ = SuccOrder.limitRecOn o (fun (a : Ordinal.{?u.73}) (ha : IsMin a) => ⋯.mpr H₁) (fun (a : Ordinal.{?u.73}) (x : ¬IsMax a) => H₂ a) H₃
Instances For
Bounded recursion on ordinals. Similar to limitRecOn
, with the assumption o < l
added to all cases. The final term's domain is the ordinals below l
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- o.orderTopToTypeSucc = OrderTop.mk ⋯
Alias of Ordinal.toType_noMax_of_succ_lt
.
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
.
Equations
- Ordinal.IsNormal f = ((∀ (o : Ordinal.{?u.21}), f o < f (Order.succ o)) ∧ ∀ (o : Ordinal.{?u.21}), o.IsLimit → ∀ (a : Ordinal.{?u.20}), f o ≤ a ↔ ∀ b < o, f b ≤ a)
Instances For
Alias of Ordinal.isNormal_add_right
.
Alias of Ordinal.isLimit_add
.
Subtraction on ordinals #
a - b
is the unique ordinal satisfying b + (a - b) = a
when b ≤ a
.
Equations
- Ordinal.sub = { sub := fun (a b : Ordinal.{?u.6}) => sInf {o : Ordinal.{?u.6} | a ≤ b + o} }
Alias of Ordinal.isLimit_sub
.
Multiplication of ordinals #
The multiplication of ordinals o₁
and o₂
is the (well founded) lexicographic order on
o₂ × o₁
.
Alias of Ordinal.isNormal_mul_right
.
Alias of Ordinal.isLimit_mul
.
Alias of Ordinal.isLimit_mul_left
.
Division on ordinals #
a / b
is the unique ordinal o
satisfying a = b * o + o'
with o' < b
.
Equations
- Ordinal.div = { div := fun (a b : Ordinal.{?u.6}) => if b = 0 then 0 else sInf {o : Ordinal.{?u.6} | a < b * Order.succ o} }
a % b
is the unique ordinal o'
satisfying
a = b * o + o'
with o' < b
.
Equations
- Ordinal.mod = { mod := fun (a b : Ordinal.{?u.5}) => a - b * (a / b) }
Families of ordinals #
There are two kinds of indexed families that naturally arise when dealing with ordinals: those indexed by some type in the appropriate universe, and those indexed by ordinals less than another. The following API allows one to convert from one kind of family to the other.
In many cases, this makes it easy to prove claims about one kind of family via the corresponding claim on the other.
Converts a family indexed by a Type u
to one indexed by an Ordinal.{u}
using a specified
well-ordering.
Equations
- Ordinal.bfamilyOfFamily' r f a ha = f ((Ordinal.enum r) ⟨a, ha⟩)
Instances For
Converts a family indexed by a Type u
to one indexed by an Ordinal.{u}
using a well-ordering
given by the axiom of choice.
Equations
- Ordinal.bfamilyOfFamily = Ordinal.bfamilyOfFamily' WellOrderingRel
Instances For
Converts a family indexed by an Ordinal.{u}
to one indexed by a Type u
using a specified
well-ordering.
Equations
- Ordinal.familyOfBFamily' r ho f i = f ((Ordinal.typein r).toRelEmbedding i) ⋯
Instances For
Converts a family indexed by an Ordinal.{u}
to one indexed by a Type u
using a well-ordering
given by the axiom of choice.
Equations
- o.familyOfBFamily f = Ordinal.familyOfBFamily' (fun (x1 x2 : o.toType) => x1 < x2) ⋯ f
Instances For
The range of a family indexed by ordinals.
Equations
- o.brange f = {a : α | ∃ (i : Ordinal.{?u.11}) (hi : i < o), f i hi = a}
Instances For
Supremum of a family of ordinals #
The range of an indexed ordinal function, whose outputs live in a higher universe than the
inputs, is always bounded above. See Ordinal.lsub
for an explicit bound.
le_ciSup
whenever the input type is small in the output universe. This lemma sometimes
fails to infer f
in simple cases and needs it to be given explicitly.
ciSup_le_iff'
whenever the input type is small in the output universe.
An alias of ciSup_le'
for discoverability.
lt_ciSup_iff'
whenever the input type is small in the output universe.
Alias of lt_iSup_iff
.
The supremum of a family of ordinals indexed by the set of ordinals less than some
o : Ordinal.{u}
. This is a special case of sup
over the family provided by
familyOfBFamily
.
Equations
- o.bsup f = Ordinal.sup (o.familyOfBFamily f)
Instances For
The least strict upper bound of a family of ordinals.
Equations
- Ordinal.lsub f = Ordinal.sup (Order.succ ∘ f)
Instances For
The least strict upper bound of a family of ordinals indexed by the set of ordinals less than
some o : Ordinal.{u}
.
This is to lsub
as bsup
is to sup
.
Equations
- o.blsub f = o.bsup fun (a : Ordinal.{?u.31}) (ha : a < o) => Order.succ (f a ha)
Instances For
A two-argument version of Ordinal.blsub
.
Deprecated. If you need this value explicitly, write it in terms of iSup
. If you just want an
upper bound for the image of op
, use that Iio a ×ˢ Iio b
is a small set.
Equations
- o₁.blsub₂ o₂ op = Ordinal.lsub fun (x : o₁.toType × o₂.toType) => op ⋯ ⋯
Instances For
Minimum excluded ordinals #
The minimum excluded ordinal in a family of ordinals.
Equations
- Ordinal.mex f = sInf (Set.range f)ᶜ
Instances For
The minimum excluded ordinal of a family of ordinals indexed by the set of ordinals less than
some o : Ordinal.{u}
. This is a special case of mex
over the family provided by
familyOfBFamily
.
This is to mex
as bsup
is to sup
.
Equations
- o.bmex f = Ordinal.mex (o.familyOfBFamily f)
Instances For
Results about injectivity and surjectivity #
The type of ordinals in universe u
is not Small.{u}
. This is the type-theoretic analog of
the Burali-Forti paradox.
Casting naturals into ordinals, compatibility with operations #
Alias of Ordinal.one_add_natCast
.
Alias of Ordinal.natCast_mul
.
Alias of Ordinal.natCast_le
.
Alias of Ordinal.natCast_inj
.
Alias of Ordinal.natCast_lt
.
Alias of Ordinal.natCast_eq_zero
.
Alias of Ordinal.natCast_ne_zero
.
Alias of Ordinal.natCast_pos
.
Alias of Ordinal.natCast_sub
.
Alias of Ordinal.natCast_div
.
Alias of Ordinal.natCast_mod
.
Alias of Ordinal.lift_natCast
.
Properties of ω #
Alias of Ordinal.lt_omega0
.
Alias of Ordinal.nat_lt_omega0
.
Alias of Ordinal.omega0_ne_zero
.
Alias of Ordinal.one_lt_omega0
.
Alias of Ordinal.isLimit_omega0
.
Alias of Ordinal.isLimit_omega0
.
Alias of Ordinal.omega0_le
.
Alias of Ordinal.sup_natCast
.
Alias of Ordinal.omega0_le_of_isLimit
.
Alias of Ordinal.one_add_omega0
.
Alias of Ordinal.add_omega0
.
Alias of Ordinal.one_add_of_omega0_le
.
Alias of Ordinal.isLimit_iff_omega0_dvd
.
Alias of Ordinal.IsNormal.apply_omega0
.
Alias of Cardinal.isLimit_ord
.