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
initial_seg r s: type of order embeddings ofrintosfor which the range is an initial segment (i.e., ifbbelongs to the range, then anyb' < balso belongs to the range). It is denoted byr ≼i s.principal_seg r s: Type of order embeddings ofrintosfor which the range is a principal segment, i.e., an interval of the form(-∞, top)for some elementtop. It is denoted byr ≺i s.ordinal: the type of ordinals (in a given universe)type r: given a well-founded orderr, this is the corresponding ordinaltypein r a: given a well-founded orderron a typeα, anda : α, the ordinal corresponding to all elements smaller thana.enum r o h: given a well-orderron a typeα, and an ordinalostrictly 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.card o: the cardinality of an ordinalo.liftlifts an ordinal in universeuto an ordinal in universemax u v. For a version registering additionally that this is an initial segment embedding, seelift.initial_seg. For a version regiserting that it is a principal segment embedding ifu < v, seelift.principal_seg.omegais the first infinite ordinal. It is the order type ofℕ.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 inordinal_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 ois the successor of the ordinalo.min: the minimal element of a nonempty indexed family of ordinalsomin: the minimal element of a nonempty set of ordinalsord c: whencis a cardinal,ord cis the smallest ordinal with this cardinality. It is the canonical way to represent a cardinal with an ordinal.
Notations
r ≼i s: the type of initial segment embeddings ofrintos.r ≺i s: the type of principal segment embeddings ofrintos.ωis a notation for the first infinite ordinal in the locale ordinal.
Initial segments
Order embeddings whose range is an initial segment of s (i.e., if b belongs to the range, then
any b' < b also belongs to the range). The type of these embeddings from r to s is called
initial_seg r s, and denoted by r ≼i s.
- to_rel_embedding : r ↪r s
- init : ∀ (a : α) (b : β), s b (⇑(c.to_rel_embedding) a) → (∃ (a' : α), ⇑(c.to_rel_embedding) a' = b)
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.
Equations
Equations
- initial_seg.has_coe_to_fun = {F := λ (_x : initial_seg r s), α → β, coe := λ (f : initial_seg r s) (x : α), ⇑↑f x}
An order isomorphism is an initial segment
Equations
- initial_seg.of_iso f = {to_rel_embedding := ↑f, init := _}
The identity function shows that ≼i is reflexive
Equations
- initial_seg.refl r = {to_rel_embedding := rel_embedding.refl r, init := _}
Composition of functions shows that ≼i is transitive
Equations
- f.trans g = {to_rel_embedding := f.to_rel_embedding.trans g.to_rel_embedding, init := _}
Equations
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
Equations
- initial_seg.cod_restrict p f H = {to_rel_embedding := rel_embedding.cod_restrict p ↑f H, init := _}
Initial segment embedding of an order r into the disjoint union of r and s.
Equations
- initial_seg.le_add r s = {to_rel_embedding := {to_embedding := {to_fun := sum.inl β, inj' := _}, map_rel_iff' := _}, init := _}
Principal segments
Order embeddings whose range is a principal segment of s (i.e., an interval of the form
(-∞, top) for some element top of β). The type of these embeddings from r to s is called
principal_seg r s, and denoted by r ≺i s. Principal segments are in particular initial
segments.
- to_rel_embedding : r ↪r s
- top : β
- down : ∀ (b : β), s b c.top ↔ ∃ (a : α), ⇑(c.to_rel_embedding) a = b
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 open interval (-∞, top) for some element top of β. Such order
embeddings are called principal segments
Equations
Equations
- principal_seg.has_coe_to_fun = {F := λ (_x : principal_seg r s), α → β, coe := λ (f : principal_seg r s), ⇑f}
A principal segment is in particular an initial segment.
Equations
- principal_seg.has_coe_initial_seg = {coe := λ (f : principal_seg r s), {to_rel_embedding := f.to_rel_embedding, init := _}}
Composition of a principal segment with an initial segment, as a principal segment
Composition of two principal segments as a principal segment
Composition of an order isomorphism with a principal segment, as a principal segment
Equations
- principal_seg.equiv_lt f g = {to_rel_embedding := ↑f.trans ↑g, top := g.top, down := _}
Composition of a principal segment with an order isomorphism, as a principal segment
Given a well order s, there is a most one principal segment embedding of r into s.
Equations
Any element of a well order yields a principal segment
Equations
- principal_seg.of_element r a = {to_rel_embedding := subrel.rel_embedding r {b : α | r b a}, top := a, down := _}
Restrict the codomain of a principal segment
Equations
- principal_seg.cod_restrict p f H H₂ = {to_rel_embedding := rel_embedding.cod_restrict p ↑f H, top := ⟨f.top, H₂⟩, down := _}
Properties of initial and principal segments
To an initial segment taking values in a well order, one can associate either a principal segment (if the range is not everything, hence one can take as top the minimum of the complement of the range) or an order isomorphism (if the range is everything).
Equations
- f.lt_or_eq = dite (function.surjective ⇑f) (λ (h : function.surjective ⇑f), sum.inr (rel_iso.of_surjective ↑f h)) (λ (h : ¬function.surjective ⇑f), have h' : ∃ (b : β), ∀ (x : β), s x b ↔ ∃ (y : α), ⇑f y = x, from _, sum.inl {to_rel_embedding := ↑f, top := classical.some h', down := _})
Composition of an initial segment taking values in a well order and a principal segment.
Given an order embedding into a well order, collapse the order embedding by filling the
gaps, to obtain an initial segment. Here, we construct the collapsed order embedding pointwise,
but the proof of the fact that it is an initial segment will be given in collapse.
Equations
- f.collapse_F = _.fix (λ (a : α) (IH : Π (y : α), r y a → {b // ¬s (⇑f y) b}), let S : set β := {b : β | ∀ (a_1 : α) (h : r a_1 a), s (IH a_1 h).val b} in ⟨is_well_order.wf.min S _, _⟩)
Construct an initial segment from an order embedding into a well order, by collapsing it to fill the gaps.
Equations
- f.collapse = {to_rel_embedding := rel_embedding.of_monotone (λ (a : α), (f.collapse_F a).val) _, init := _}
Well order on an arbitrary type
An embedding of any type to the set of cardinals.
Any type can be endowed with a well order, obtained by pulling back the well order over cardinals by some embedding.
Equations
Equations
Definition of ordinals
- α : Type ?
- r : c.α → c.α → Prop
- wo : is_well_order c.α c.r
Bundled structure registering a well order on a type. Ordinals will be defined as a quotient of this type.
Equivalence relation on well orders on arbitrary types in universe u, given by order
isomorphism.
Equations
- ordinal.is_equivalent = {r := λ (_x : Well_order), ordinal.is_equivalent._match_2 _x, iseqv := ordinal.is_equivalent._proof_1}
- ordinal.is_equivalent._match_2 {α := α, r := r, wo := wo} = λ (_x : Well_order), ordinal.is_equivalent._match_1 α r _x
- ordinal.is_equivalent._match_1 α r {α := β, r := s, wo := wo'} = nonempty (r ≃r s)
The order type of a well order is an ordinal.
The order type of an element inside a well order. For the embedding as a principal segment, see
typein.principal_seg.
Equations
- ordinal.typein r a = ordinal.type (subrel r {b : α | r b a})
The order on ordinals
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.
Equations
- a.le b = quotient.lift_on₂ a b (λ (_x : Well_order), ordinal.le._match_2 _x) ordinal.le._proof_1
- ordinal.le._match_2 {α := α, r := r, wo := wo} = λ (_x : Well_order), ordinal.le._match_1 α r _x
- ordinal.le._match_1 α r {α := β, r := s, wo := wo'} = nonempty (initial_seg r s)
Equations
- ordinal.has_le = {le := ordinal.le}
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.
Equations
- a.lt b = quotient.lift_on₂ a b (λ (_x : Well_order), ordinal.lt._match_2 _x) ordinal.lt._proof_1
- ordinal.lt._match_2 {α := α, r := r, wo := wo} = λ (_x : Well_order), ordinal.lt._match_1 α r _x
- ordinal.lt._match_1 α r {α := β, r := s, wo := wo'} = nonempty (principal_seg r s)
Equations
- ordinal.has_lt = {lt := ordinal.lt}
Equations
- ordinal.partial_order = {le := has_le.le ordinal.has_le, lt := has_lt.lt ordinal.has_lt, le_refl := ordinal.partial_order._proof_1, le_trans := ordinal.partial_order._proof_2, lt_iff_le_not_le := ordinal.partial_order._proof_3, le_antisymm := ordinal.partial_order._proof_4}
Given two ordinals α ≤ β, then initial_seg_out α β is the initial segment embedding
of α to β, as map from a model type for α to a model type for β.
Equations
- ordinal.initial_seg_out h = (quotient.out α).cases_on (λ (α_1 : Type u_1) (r : α_1 → α_1 → Prop) (wo : is_well_order α_1 r), (quotient.out β).cases_on (λ (α_2 : Type u_1) (r_1 : α_2 → α_2 → Prop) (wo_1 : is_well_order α_2 r_1), classical.choice)) _
Given two ordinals α < β, then principal_seg_out α β is the principal segment embedding
of α to β, as map from a model type for α to a model type for β.
Equations
- ordinal.principal_seg_out h = (quotient.out α).cases_on (λ (α_1 : Type u_1) (r : α_1 → α_1 → Prop) (wo : is_well_order α_1 r), (quotient.out β).cases_on (λ (α_2 : Type u_1) (r_1 : α_2 → α_2 → Prop) (wo_1 : is_well_order α_2 r_1), classical.choice)) _
Given two ordinals α = β, then rel_iso_out α β is the order isomorphism between two
model types for α and β.
Equations
- ordinal.rel_iso_out h = (quotient.out α).cases_on (λ (α_1 : Type u_1) (r : α_1 → α_1 → Prop) (wo : is_well_order α_1 r), (quotient.out β).cases_on (λ (α_2 : Type u_1) (r_1 : α_2 → α_2 → Prop) (wo_1 : is_well_order α_2 r_1), classical.choice ∘ _)) _
Enumerating elements in a well-order with ordinals.
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 o = quot.rec_on o (λ (_x : Well_order), ordinal.enum._match_1 r _x) _
- ordinal.enum._match_1 r {α := β, r := s, wo := _x} = λ (h : quot.mk setoid.r {α := β, r := s, wo := _x} < ordinal.type r), (classical.choice h).top
A well order r is order isomorphic to the set of ordinals strictly smaller than the
ordinal version of r.
Equations
- ordinal.typein_iso r = {to_equiv := {to_fun := λ (x : α), ⟨ordinal.typein r x, _⟩, inv_fun := λ (x : ↥(λ (_x : ordinal), _x < ordinal.type r)), ordinal.enum r x.val _, left_inv := _, right_inv := _}, map_rel_iff' := _}
Equations
Principal segment version of the typein function, embedding a well order into
ordinals as a principal segment.
Equations
- ordinal.typein.principal_seg r = {to_rel_embedding := rel_embedding.of_monotone (ordinal.typein r) _, top := ordinal.type r _inst_1, down := _}
Cardinality of ordinals
The cardinal of an ordinal is the cardinal of any set with that order type.
Equations
- o.card = quot.lift_on o (λ (_x : Well_order), ordinal.card._match_1 _x) ordinal.card._proof_1
- ordinal.card._match_1 {α := α, r := r, wo := _x} = cardinal.mk α
Equations
- ordinal.inhabited = {default := 0}
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 lift.initial_seg.
Equations
- o.lift = quotient.lift_on o (λ (_x : Well_order), ordinal.lift._match_2 _x) ordinal.lift._proof_1
- ordinal.lift._match_2 {α := α, r := r, wo := wo} = ordinal.type (⇑equiv.ulift ⁻¹'o r)
Initial segment version of the lift operation on ordinals, embedding ordinal.{u} in
ordinal.{v} as an initial segment when u ≤ v.
Equations
- ordinal.lift.initial_seg = {to_rel_embedding := {to_embedding := {to_fun := ordinal.lift, inj' := ordinal.lift.initial_seg._proof_1}, map_rel_iff' := ordinal.lift.initial_seg._proof_2}, init := ordinal.lift.initial_seg._proof_3}
The first infinite ordinal omega
ω is the first infinite ordinal, defined as the order type of ℕ.
Equations
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
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
- ordinal.has_add = {add := λ (o₁ o₂ : ordinal), quotient.lift_on₂ o₁ o₂ (λ (_x : Well_order), ordinal.has_add._match_4 _x) ordinal.has_add._proof_1}
- ordinal.has_add._match_4 {α := α, r := r, wo := wo} = λ (_x : Well_order), ordinal.has_add._match_3 α r wo _x
- ordinal.has_add._match_3 α r wo {α := β, r := s, wo := wo'} = ⟦{α := α ⊕ β, r := sum.lex r s, wo := _}⟧
Equations
- ordinal.add_monoid = {add := has_add.add ordinal.has_add, add_assoc := ordinal.add_monoid._proof_1, zero := 0, zero_add := ordinal.add_monoid._proof_2, add_zero := ordinal.add_monoid._proof_3}
Equations
- ordinal.decidable_linear_order = {le := partial_order.le ordinal.partial_order, lt := partial_order.lt ordinal.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := ordinal.le_total, decidable_le := classical.dec_rel has_le.le, decidable_eq := decidable_eq_of_decidable_le (classical.dec_rel has_le.le), decidable_lt := decidable_lt_of_decidable_le (classical.dec_rel has_le.le)}
Equations
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
Principal segment version of the lift operation on ordinals, embedding ordinal.{u} in
ordinal.{v} as a principal segment when u < v.
Equations
- ordinal.lift.principal_seg = {to_rel_embedding := ↑ordinal.lift.initial_seg, top := ordinal.univ, down := ordinal.lift.principal_seg._proof_1}
Minimum
The minimal element of a nonempty family of ordinals
Equations
- ordinal.min I f = ordinal.wf.min (set.range f) _
- _ = _
The minimal element of a nonempty set of ordinals
Equations
- ordinal.omin S H = ordinal.min _ subtype.val
- _ = _
Representing a cardinal with an ordinal
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 = let ι : Type u_1 → Type u_1 := λ (α : Type u_1), {r // is_well_order α r}, F : Type u_1 → ordinal := λ (α : Type u_1), ordinal.min _ (λ (i : ι α), ⟦{α := α, r := i.val, wo := _}⟧) in quot.lift_on c F cardinal.ord._proof_3
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.order_embedding = (rel_embedding.of_monotone cardinal.ord cardinal.ord.order_embedding._proof_2).order_embedding_of_lt_embedding
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).