mathlib3 documentation

set_theory.ordinal.basic

Ordinals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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 #

Well order on an arbitrary type #

noncomputable def embedding_to_cardinal {σ : Type u} :

An embedding of any type to the set of cardinals.

Equations
def well_ordering_rel {σ : Type u} :
σ σ Prop

Any type can be endowed with a well order, obtained by pulling back the well order over cardinals by some embedding.

Equations
Instances for well_ordering_rel
@[protected, instance]
@[protected, instance]

Definition of ordinals #

structure Well_order  :
Type (u+1)

Bundled structure registering a well order on a type. Ordinals will be defined as a quotient of this type.

Instances for Well_order
@[protected, instance]
Equations
@[simp]
theorem Well_order.eta (o : Well_order) :
{α := o.α, r := o.r, wo := _} = o
@[protected, instance]

Equivalence relation on well orders on arbitrary types in universe u, given by order isomorphism.

Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def linear_order_out (o : ordinal) :
Equations
@[protected, instance]
def ordinal.type {α : Type u_1} (r : α α Prop) [wo : is_well_order α r] :

The order type of a well order is an ordinal.

Equations
@[protected, instance]
Equations
def ordinal.typein {α : Type u_1} (r : α α Prop) [is_well_order α r] (a : α) :

The order type of an element inside a well order. For the embedding as a principal segment, see typein.principal_seg.

Equations
@[simp]
@[simp]
theorem ordinal.type_def {α : Type u_1} (r : α α Prop) [wo : is_well_order α r] :
{α := α, r := r, wo := wo} = ordinal.type r
@[simp]
theorem ordinal.type_eq {α β : Type u_1} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] :
theorem rel_iso.ordinal_type_eq {α β : Type u_1} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] (h : r ≃r s) :
@[simp]
theorem ordinal.type_eq_zero_of_empty {α : Type u_1} (r : α α Prop) [is_well_order α r] [is_empty α] :
@[simp]
theorem ordinal.type_eq_zero_iff_is_empty {α : Type u_1} {r : α α Prop} [is_well_order α r] :
theorem ordinal.type_ne_zero_iff_nonempty {α : Type u_1} {r : α α Prop} [is_well_order α r] :
theorem ordinal.type_ne_zero_of_nonempty {α : Type u_1} (r : α α Prop) [is_well_order α r] [h : nonempty α] :
theorem ordinal.type_eq_one_of_unique {α : Type u_1} (r : α α Prop) [is_well_order α r] [unique α] :
@[simp]
theorem ordinal.type_eq_one_iff_unique {α : Type u_1} {r : α α Prop} [is_well_order α r] :
@[protected, instance]
@[protected]
theorem ordinal.one_ne_zero  :
1 0
@[protected, instance]
@[simp]
theorem ordinal.type_preimage {α β : Type u} (r : α α Prop) [is_well_order α r] (f : β α) :
theorem ordinal.induction_on {C : ordinal Prop} (o : ordinal) (H : (α : Type u_1) (r : α α Prop) [_inst_1 : is_well_order α r], C (ordinal.type r)) :
C o

The order on ordinals #

@[protected, instance]
Equations
theorem ordinal.type_le_iff {α β : Type u_1} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] :
theorem ordinal.type_le_iff' {α β : Type u_1} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] :
theorem initial_seg.ordinal_type_le {α β : Type u_1} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] (h : initial_seg r s) :
theorem rel_embedding.ordinal_type_le {α β : Type u_1} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] (h : r ↪r s) :
@[simp]
theorem ordinal.type_lt_iff {α β : Type u_1} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] :
theorem principal_seg.ordinal_type_lt {α β : Type u_1} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] (h : principal_seg r s) :
@[protected]
theorem ordinal.zero_le (o : ordinal) :
0 o
@[protected, instance]
Equations
@[simp]
theorem ordinal.bot_eq_zero  :
= 0
@[protected, simp]
theorem ordinal.le_zero {o : ordinal} :
o 0 o = 0
@[protected]
theorem ordinal.pos_iff_ne_zero {o : ordinal} :
0 < o o 0
@[protected]
theorem ordinal.not_lt_zero (o : ordinal) :
¬o < 0
theorem ordinal.eq_zero_or_pos (a : ordinal) :
a = 0 0 < a
@[protected, instance]
Equations
@[protected, instance]
noncomputable def ordinal.initial_seg_out {α β : ordinal} (h : α β) :

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
noncomputable def ordinal.principal_seg_out {α β : ordinal} (h : α < β) :

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
theorem ordinal.typein_lt_type {α : Type u_1} (r : α α Prop) [is_well_order α r] (a : α) :
@[simp]
theorem ordinal.typein_top {α β : Type u_1} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] (f : principal_seg r s) :
@[simp]
theorem ordinal.typein_apply {α β : Type u_1} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] (f : initial_seg r s) (a : α) :
@[simp]
theorem ordinal.typein_lt_typein {α : Type u_1} (r : α α Prop) [is_well_order α r] {a b : α} :
theorem ordinal.typein_surj {α : Type u_1} (r : α α Prop) [is_well_order α r] {o : ordinal} (h : o < ordinal.type r) :
(a : α), ordinal.typein r a = o
theorem ordinal.typein_injective {α : Type u_1} (r : α α Prop) [is_well_order α r] :
@[simp]
theorem ordinal.typein_inj {α : Type u_1} (r : α α Prop) [is_well_order α r] {a b : α} :

Enumerating elements in a well-order with ordinals. #

noncomputable def ordinal.enum {α : Type u_1} (r : α α Prop) [is_well_order α r] (o : ordinal) :

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
theorem ordinal.enum_type {α β : Type u_1} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] (f : principal_seg s r) {h : ordinal.type s < ordinal.type r} :
@[simp]
theorem ordinal.enum_typein {α : Type u_1} (r : α α Prop) [is_well_order α r] (a : α) :
@[simp]
theorem ordinal.typein_enum {α : Type u_1} (r : α α Prop) [is_well_order α r] {o : ordinal} (h : o < ordinal.type r) :
theorem ordinal.enum_lt_enum {α : Type u_1} {r : α α Prop} [is_well_order α r] {o₁ o₂ : ordinal} (h₁ : o₁ < ordinal.type r) (h₂ : o₂ < ordinal.type r) :
r (ordinal.enum r o₁ h₁) (ordinal.enum r o₂ h₂) o₁ < o₂
theorem ordinal.rel_iso_enum' {α β : Type u} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] (f : r ≃r s) (o : ordinal) (hr : o < ordinal.type r) (hs : o < ordinal.type s) :
f (ordinal.enum r o hr) = ordinal.enum s o hs
theorem ordinal.rel_iso_enum {α β : Type u} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] (f : r ≃r s) (o : ordinal) (hr : o < ordinal.type r) :
f (ordinal.enum r o hr) = ordinal.enum s o _
theorem ordinal.induction {p : ordinal Prop} (i : ordinal) (h : (j : ordinal), ( (k : ordinal), k < j p k) p j) :
p i

Reformulation of well founded induction on ordinals as a lemma that works with the induction tactic, as in induction i using ordinal.induction with i IH.

def ordinal.typein.principal_seg {α : Type u} (r : α α Prop) [is_well_order α r] :

Principal segment version of the typein function, embedding a well order into ordinals as a principal segment.

Equations

Cardinality of ordinals #

The cardinal of an ordinal is the cardinality of any type on which a relation with that order type is defined.

Equations
@[simp]
theorem ordinal.card_type {α : Type u_1} (r : α α Prop) [is_well_order α r] :
@[simp]
theorem ordinal.card_typein {α : Type u_1} {r : α α Prop} [wo : is_well_order α r] (x : α) :
cardinal.mk {y // r y x} = (ordinal.typein r x).card
theorem ordinal.card_le_card {o₁ o₂ : ordinal} :
o₁ o₂ o₁.card o₂.card
@[simp]
theorem ordinal.card_zero  :
0.card = 0
@[simp]
theorem ordinal.card_eq_zero {o : ordinal} :
o.card = 0 o = 0
@[simp]
theorem ordinal.card_one  :
1.card = 1

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
@[simp]
theorem ordinal.type_ulift {α : Type u_1} (r : α α Prop) [is_well_order α r] :
theorem rel_iso.ordinal_lift_type_eq {α : Type u} {β : Type v} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] (f : r ≃r s) :
@[simp]
theorem ordinal.type_lift_preimage {α : Type u} {β : Type v} (r : α α Prop) [is_well_order α r] (f : β α) :
@[simp]

lift.{(max u v) u} equals lift.{v u}. Using set_option pp.universes true will make it much easier to understand what's happening when using this lemma.

@[simp]

lift.{(max v u) u} equals lift.{v u}. Using set_option pp.universes true will make it much easier to understand what's happening when using this lemma.

@[simp]
theorem ordinal.lift_id' (a : ordinal) :
a.lift = a

An ordinal lifted to a lower or equal universe equals itself.

@[simp]
theorem ordinal.lift_id (a : ordinal) :
a.lift = a

An ordinal lifted to the same universe equals itself.

@[simp]
theorem ordinal.lift_uzero (a : ordinal) :
a.lift = a

An ordinal lifted to the zero universe equals itself.

@[simp]
theorem ordinal.lift_lift (a : ordinal) :
theorem ordinal.lift_type_le {α : Type u} {β : Type v} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] :
theorem ordinal.lift_type_eq {α : Type u} {β : Type v} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] :
theorem ordinal.lift_type_lt {α : Type u} {β : Type v} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] :
@[simp]
theorem ordinal.lift_le {a b : ordinal} :
a.lift b.lift a b
@[simp]
theorem ordinal.lift_inj {a b : ordinal} :
a.lift = b.lift a = b
@[simp]
theorem ordinal.lift_lt {a b : ordinal} :
a.lift < b.lift a < b
@[simp]
theorem ordinal.lift_zero  :
0.lift = 0
@[simp]
theorem ordinal.lift_one  :
1.lift = 1
@[simp]
theorem ordinal.lift_card (a : ordinal) :
theorem ordinal.lift_down' {a : cardinal} {b : ordinal} (h : b.card a.lift) :
(a' : ordinal), a'.lift = b
theorem ordinal.lift_down {a : ordinal} {b : ordinal} (h : b a.lift) :
(a' : ordinal), a'.lift = b
theorem ordinal.le_lift_iff {a : ordinal} {b : ordinal} :
b a.lift (a' : ordinal), a'.lift = b a' a
theorem ordinal.lt_lift_iff {a : ordinal} {b : ordinal} :
b < a.lift (a' : ordinal), a'.lift = b a' < a

Initial segment version of the lift operation on ordinals, embedding ordinal.{u} in ordinal.{v} as an initial segment when u ≤ v.

Equations

The first infinite ordinal omega #

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

Equations
@[simp]

Note that the presence of this lemma makes simp [omega] form a loop.

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.

@[protected, instance]

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
@[protected, instance]
Equations
@[simp]
theorem ordinal.card_add (o₁ o₂ : ordinal) :
(o₁ + o₂).card = o₁.card + o₂.card
@[simp]
theorem ordinal.type_sum_lex {α β : Type u} (r : α α Prop) (s : β β Prop) [is_well_order α r] [is_well_order β s] :
@[simp]
theorem ordinal.card_nat (n : ) :
theorem ordinal.le_add_right (a b : ordinal) :
a a + b
theorem ordinal.le_add_left (a b : ordinal) :
a b + a
@[protected, instance]
@[simp]
@[simp]
@[simp]
theorem ordinal.max_eq_zero {a b : ordinal} :
linear_order.max a b = 0 a = 0 b = 0
@[simp]
@[protected, instance]
@[protected, instance]
noncomputable def ordinal.succ_order  :
Equations
@[simp]
theorem ordinal.add_one_eq_succ (o : ordinal) :
o + 1 = order.succ o
@[simp]
theorem ordinal.succ_zero  :
@[simp]
theorem ordinal.succ_one  :
theorem ordinal.add_succ (o₁ o₂ : ordinal) :
o₁ + order.succ o₂ = order.succ (o₁ + o₂)
theorem ordinal.one_le_iff_pos {o : ordinal} :
1 o 0 < o
theorem ordinal.one_le_iff_ne_zero {o : ordinal} :
1 o o 0
theorem ordinal.succ_pos (o : ordinal) :
theorem ordinal.lt_one_iff_zero {a : ordinal} :
a < 1 a = 0
theorem ordinal.le_one_iff {a : ordinal} :
a 1 a = 0 a = 1
@[simp]
theorem ordinal.card_succ (o : ordinal) :
@[protected, instance]
Equations
@[protected, instance]
noncomputable def ordinal.unique_out_one  :
Equations

Extra properties of typein and enum #

@[simp]
theorem ordinal.typein_le_typein {α : Type u_1} (r : α α Prop) [is_well_order α r] {x x' : α} :
@[simp]
theorem ordinal.enum_le_enum {α : Type u_1} (r : α α Prop) [is_well_order α r] {o o' : ordinal} (ho : o < ordinal.type r) (ho' : o' < ordinal.type r) :
¬r (ordinal.enum r o' ho') (ordinal.enum r o ho) o o'
theorem ordinal.enum_zero_le {α : Type u_1} {r : α α Prop} [is_well_order α r] (h0 : 0 < ordinal.type r) (a : α) :
¬r a (ordinal.enum r 0 h0)
theorem ordinal.enum_zero_le' {o : ordinal} (h0 : 0 < o) (a : (quotient.out o).α) :
@[simp]
theorem ordinal.enum_inj {α : Type u_1} {r : α α Prop} [is_well_order α r] {o₁ o₂ : ordinal} (h₁ : o₁ < ordinal.type r) (h₂ : o₂ < ordinal.type r) :
ordinal.enum r o₁ h₁ = ordinal.enum r o₂ h₂ o₁ = o₂
noncomputable def ordinal.enum_iso {α : Type u_1} (r : α α Prop) [is_well_order α r] :

A well order r is order isomorphic to the set of ordinals smaller than type r.

Equations
@[simp]
theorem ordinal.enum_iso_apply {α : Type u_1} (r : α α Prop) [is_well_order α r] (x : (λ (_x : ordinal), _x < ordinal.type r)) :
@[simp]
theorem ordinal.enum_iso_symm_apply_coe {α : Type u_1} (r : α α Prop) [is_well_order α r] (x : α) :
noncomputable def ordinal.enum_iso_out (o : ordinal) :

The order isomorphism between ordinals less than o and o.out.α.

Equations
noncomputable def ordinal.out_order_bot_of_pos {o : ordinal} (ho : 0 < o) :

o.out.α is an order_bot whenever 0 < o.

Equations

Universal ordinal #

@[nolint]

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

Representing a cardinal with an ordinal #

noncomputable def cardinal.ord (c : cardinal) :

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
theorem cardinal.ord_eq_Inf (α : Type u) :
theorem cardinal.ord_eq (α : Type u_1) :
(r : α α Prop) [wo : is_well_order α r], (cardinal.mk α).ord = ordinal.type r
theorem cardinal.ord_le_type {α : Type u_1} (r : α α Prop) [h : is_well_order α r] :
theorem cardinal.ord_le {c : cardinal} {o : ordinal} :
c.ord o c o.card
theorem cardinal.lt_ord {c : cardinal} {o : ordinal} :
o < c.ord o.card < c
@[simp]
theorem cardinal.card_ord (c : cardinal) :
c.ord.card = c

Galois coinsertion between cardinal.ord and ordinal.card.

Equations
@[simp]
theorem cardinal.ord_le_ord {c₁ c₂ : cardinal} :
c₁.ord c₂.ord c₁ c₂
@[simp]
theorem cardinal.ord_lt_ord {c₁ c₂ : cardinal} :
c₁.ord < c₂.ord c₁ < c₂
@[simp]
theorem cardinal.ord_zero  :
0.ord = 0
@[simp]
theorem cardinal.ord_nat (n : ) :
@[simp]
theorem cardinal.ord_one  :
1.ord = 1
@[simp]
theorem cardinal.lift_ord (c : cardinal) :
theorem cardinal.card_typein_lt {α : Type u_1} (r : α α Prop) [is_well_order α r] (x : α) (h : (cardinal.mk α).ord = ordinal.type r) :

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
@[nolint]

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).

Equations
@[simp]
theorem ordinal.nat_le_card {o : ordinal} {n : } :
@[simp]
theorem ordinal.nat_lt_card {o : ordinal} {n : } :
n < o.card n < o
@[simp]
theorem ordinal.card_lt_nat {o : ordinal} {n : } :
o.card < n o < n
@[simp]
theorem ordinal.card_le_nat {o : ordinal} {n : } :
@[simp]
theorem ordinal.card_eq_nat {o : ordinal} {n : } :
o.card = n o = n
@[simp]
theorem ordinal.type_fintype {α : Type u_1} (r : α α Prop) [is_well_order α r] [fintype α] :