Ordinals #
Ordinals are defined as equivalences of well-ordered sets under order isomorphism. They are endowed with a total order, where an ordinal is smaller than another one if it embeds into it as an initial segment (or, equivalently, in any way). This total order is well founded.
Main definitions #
Ordinal
: the type of ordinals (in a given universe)Ordinal.type r
: given a well-founded orderr
, this is the corresponding ordinalOrdinal.typein r a
: given a well-founded orderr
on a typeα
, anda : α
, the ordinal corresponding to all elements smaller thana
.enum r ⟨o, h⟩
: given a well-orderr
on a typeα
, and an ordinalo
strictly smaller than the ordinal corresponding tor
(this is the assumptionh
), returns theo
-th element ofα
. In other words, the elements ofα
can be enumerated using ordinals up totype r
.Ordinal.card o
: the cardinality of an ordinalo
.Ordinal.lift
lifts an ordinal in universeu
to an ordinal in universemax u v
. For a version registering additionally that this is an initial segment embedding, seeOrdinal.liftInitialSeg
. For a version registering that it is a principal segment embedding ifu < v
, seeOrdinal.liftPrincipalSeg
.Ordinal.omega0
orω
is the order type ofℕ
. It is called this to matchCardinal.aleph0
and so that the omega function can be namedOrdinal.omega
. This definition is universe polymorphic:Ordinal.omega0.{u} : Ordinal.{u}
(contrast withℕ : Type
, which lives in a specific universe). In some cases the universe level has to be given explicitly.o₁ + o₂
is the order on the disjoint union ofo₁
ando₂
obtained by declaring that every element ofo₁
is smaller than every element ofo₂
. The main properties of addition (and the other operations on ordinals) are stated and proved inMathlib/SetTheory/Ordinal/Arithmetic.lean
. Here, we only introduce it and prove its basic properties to deduce the fact that the order on ordinals is total (and well founded).succ o
is the successor of the ordinalo
.Cardinal.ord c
: whenc
is a cardinal,ord c
is the smallest ordinal with this cardinality. It is the canonical way to represent a cardinal with an ordinal.
A conditionally complete linear order with bot structure is registered on ordinals, where ⊥
is
0
, the ordinal corresponding to the empty type, and Inf
is the minimum for nonempty sets and 0
for the empty set by convention.
Notations #
ω
is a notation for the first infinite ordinal in the localeOrdinal
.
Definition of ordinals #
Bundled structure registering a well order on a type. Ordinals will be defined as a quotient of this type.
- α : Type u
The underlying type of the order.
- r : self.α → self.α → Prop
The underlying relation of the order.
- wo : IsWellOrder self.α self.r
Instances For
Equations
- WellOrder.inhabited = { default := { α := PEmpty.{?u.3 + 1} , r := EmptyRelation, wo := WellOrder.inhabited.proof_1 } }
Equivalence relation on well orders on arbitrary types in universe u
, given by order
isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Ordinal.{u}
is the type of well orders in Type u
, up to order isomorphism.
Equations
Instances For
A "canonical" type order-isomorphic to the ordinal o
, living in the same universe. This is
defined through the axiom of choice.
Use this over Iio o
only when it is paramount to have a Type u
rather than a Type (u + 1)
.
Equations
- o.toType = (Quotient.out o).α
Instances For
Equations
- hasWellFounded_toType o = { rel := (Quotient.out o).r, wf := ⋯ }
Equations
Equations
- ⋯ = ⋯
Basic properties of the order type #
The order type of a well order is an ordinal.
Equations
- Ordinal.type r = ⟦{ α := α, r := r, wo := wo }⟧
Instances For
Equations
- Ordinal.zero = { zero := Ordinal.type EmptyRelation }
Equations
- Ordinal.inhabited = { default := 0 }
Equations
- Ordinal.one = { one := Ordinal.type EmptyRelation }
The order type of an element inside a well order. For the embedding as a principal segment, see
typein.principalSeg
.
Equations
- Ordinal.typein r a = Ordinal.type (Subrel r {b : α | r b a})
Instances For
Alias of Ordinal.toType_empty_iff_eq_zero
.
Equations
Alias of Ordinal.toType_nonempty_iff_ne_zero
.
The order on ordinals #
For Ordinal
:
- less-equal is defined such that well orders
r
ands
satisfytype r ≤ type s
if there exists a function embeddingr
as an initial segment ofs
. - less-than is defined such that well orders
r
ands
satisfytype r < type s
if there exists a function embeddingr
as a principal segment ofs
.
Note that most of the relevant results on initial and principal segments are proved in the
Order.InitialSeg
file.
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
Given two ordinals α ≤ β
, then initialSegToType α β
is the initial segment embedding of
α.toType
into β.toType
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of Ordinal.initialSegToType
.
Given two ordinals α ≤ β
, then initialSegToType α β
is the initial segment embedding of
α.toType
into β.toType
.
Instances For
Given two ordinals α < β
, then principalSegToType α β
is the principal segment embedding
of α.toType
into β.toType
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of Ordinal.principalSegToType
.
Given two ordinals α < β
, then principalSegToType α β
is the principal segment embedding
of α.toType
into β.toType
.
Instances For
Principal segment version of the typein
function, embedding a well order into ordinals as a
principal segment.
Equations
- Ordinal.typein.principalSeg r = { toFun := Ordinal.typein r, inj' := ⋯, map_rel_iff' := ⋯, top := Ordinal.type r, down' := ⋯ }
Instances For
Enumerating elements in a well-order with ordinals. #
A well order r
is order-isomorphic to the set of ordinals smaller than type r
.
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 α
.
Equations
- Ordinal.enum r = (Ordinal.typein.principalSeg r).subrelIso
Instances For
Equations
- Ordinal.wellFoundedRelation = { rel := fun (x1 x2 : Ordinal.{?u.5}) => x1 < x2, wf := Ordinal.lt_wf }
Equations
Reformulation of well founded induction on ordinals as a lemma that works with the
induction
tactic, as in induction i using Ordinal.induction with | h i IH => ?_
.
Cardinality of ordinals #
The cardinal of an ordinal is the cardinality of any type on which a relation with that order type is defined.
Instances For
Lifting ordinals to a higher universe #
The universe lift operation for ordinals, which embeds Ordinal.{u}
as
a proper initial segment of Ordinal.{v}
for v > u
. For the initial segment version,
see liftInitialSeg
.
Equations
- Ordinal.lift.{?u.12, ?u.11} o = Quotient.liftOn o (fun (w : WellOrder) => Ordinal.type (ULift.down ⁻¹'o w.r)) Ordinal.lift.proof_2
Instances For
lift.{max u v, u}
equals lift.{v, u}
.
Unfortunately, the simp lemma doesn't seem to work.
lift.{max v u, u}
equals lift.{v, u}
.
Unfortunately, the simp lemma doesn't seem to work.
An ordinal lifted to a lower or equal universe equals itself.
Unfortunately, the simp lemma doesn't work.
An ordinal lifted to the same universe equals itself.
An ordinal lifted to the zero universe equals itself.
Initial segment version of the lift operation on ordinals, embedding ordinal.{u}
in
ordinal.{v}
as an initial segment when u ≤ v
.
Equations
- Ordinal.liftInitialSeg = { toFun := Ordinal.lift.{?u.23, ?u.24} , inj' := Ordinal.liftInitialSeg.proof_1, map_rel_iff' := ⋯, mem_range_of_rel' := Ordinal.liftInitialSeg.proof_2 }
Instances For
Alias of Ordinal.liftInitialSeg
.
Initial segment version of the lift operation on ordinals, embedding ordinal.{u}
in
ordinal.{v}
as an initial segment when u ≤ v
.
Instances For
The first infinite ordinal ω #
ω
is the first infinite ordinal, defined as the order type of ℕ
.
Equations
- Ordinal.omega0 = Ordinal.lift.{?u.5, 0} (Ordinal.type fun (x1 x2 : ℕ) => x1 < x2)
Instances For
Alias of Ordinal.omega0
.
ω
is the first infinite ordinal, defined as the order type of ℕ
.
Equations
Instances For
ω
is the first infinite ordinal, defined as the order type of ℕ
.
Equations
- Ordinal.termω = Lean.ParserDescr.node `Ordinal.termω 1024 (Lean.ParserDescr.symbol "ω")
Instances For
Note that the presence of this lemma makes simp [omega0]
form a loop.
Alias of Ordinal.card_omega0
.
Alias of Ordinal.lift_omega0
.
Definition and first properties of addition on ordinals #
In this paragraph, we introduce the addition on ordinals, and prove just enough properties to
deduce that the order on ordinals is total (and therefore well-founded). Further properties of
the addition, together with properties of the other operations, are proved in
Mathlib/SetTheory/Ordinal/Arithmetic.lean
.
o₁ + o₂
is the order on the disjoint union of o₁
and o₂
obtained by declaring that
every element of o₁
is smaller than every element of o₂
.
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
Successor order properties #
Equations
- Ordinal.instSuccOrder = SuccOrder.ofSuccLeIff (fun (o : Ordinal.{?u.6}) => o + 1) ⋯
Alias of Ordinal.natCast_succ
.
Equations
- Ordinal.uniqueIioOne = { default := ⟨0, Ordinal.uniqueIioOne.proof_1⟩, uniq := Ordinal.uniqueIioOne.proof_2 }
Equations
- Ordinal.uniqueToTypeOne = { default := (Ordinal.enum fun (x1 x2 : Ordinal.toType 1) => x1 < x2) ⟨0, Ordinal.uniqueToTypeOne.proof_4⟩, uniq := Ordinal.uniqueToTypeOne.proof_5 }
Alias of Ordinal.one_toType_eq
.
Extra properties of typein and enum #
Alias of Ordinal.typein_one_toType
.
The order isomorphism between ordinals less than o
and o.toType
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of Ordinal.enumIsoToType
.
The order isomorphism between ordinals less than o
and o.toType
.
Equations
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Alias of Ordinal.toTypeOrderBotOfPos
.
o.toType
is an OrderBot
whenever 0 < o
.
Instances For
Universal ordinal #
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.
Equations
- Ordinal.univ.{?u.2, ?u.1} = Ordinal.lift.{?u.1, ?u.2 + 1} (Ordinal.type fun (x1 x2 : Ordinal.{?u.2}) => x1 < x2)
Instances For
Principal segment version of the lift operation on ordinals, embedding ordinal.{u}
in
ordinal.{v}
as a principal segment when u < v
.
Equations
- Ordinal.liftPrincipalSeg = { toRelEmbedding := Ordinal.liftInitialSeg.toRelEmbedding, top := Ordinal.univ.{?u.26, ?u.25} , down' := Ordinal.liftPrincipalSeg.proof_1 }
Instances For
Alias of Ordinal.liftPrincipalSeg
.
Principal segment version of the lift operation on ordinals, embedding ordinal.{u}
in
ordinal.{v}
as a principal segment when u < v
.
Instances For
Representing a cardinal with an ordinal #
Alias of Cardinal.mk_toType
.
The ordinal corresponding to a cardinal c
is the least ordinal
whose cardinal is c
. For the order-embedding version, see ord.order_embedding
.
Equations
- c.ord = Quot.liftOn c (fun (α : Type ?u.18) => ⨅ (r : { r : α → α → Prop // IsWellOrder α r }), Ordinal.type ↑r) Cardinal.ord.proof_2
Instances For
Galois coinsertion between Cardinal.ord
and Ordinal.card
.
Equations
- Cardinal.gciOrdCard = Cardinal.gc_ord_card.toGaloisCoinsertion Cardinal.gciOrdCard.proof_1
Instances For
A variation on Cardinal.lt_ord
using ≤
: If o
is no greater than the
initial ordinal of cardinality c
, then its cardinal is no greater than c
.
The converse, however, is false (for instance, o = ω+1
and c = ℵ₀
).
Alias of Cardinal.mk_ord_toType
.
Alias of Cardinal.card_typein_toType_lt
.
Alias of Cardinal.mk_Iio_ord_toType
.
The ordinal corresponding to a cardinal c
is the least ordinal
whose cardinal is c
. This is the order-embedding version. For the regular function, see ord
.
Equations
- Cardinal.ord.orderEmbedding = (RelEmbedding.ofMonotone Cardinal.ord Cardinal.ord.orderEmbedding.proof_2).orderEmbeddingOfLTEmbedding