# mathlibdocumentation

set_theory.ordinal

# 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 of r into s for which the range is an initial segment (i.e., if b belongs to the range, then any b' < b also belongs to the range). It is denoted by r ≼i s.

• principal_seg r s: Type of order embeddings of r into s for which the range is a principal segment, i.e., an interval of the form (-∞, top) for some element top. It is denoted by r ≺i s.

• ordinal: the type of ordinals (in a given universe)

• ordinal.type r: given a well-founded order r, this is the corresponding ordinal

• ordinal.typein r a: given a well-founded order r on a type α, and a : α, the ordinal corresponding to all elements smaller than a.

• enum r o h: given a well-order r on a type α, and an ordinal o strictly smaller than the ordinal corresponding to r (this is the assumption h), returns the o-th element of α. In other words, the elements of α can be enumerated using ordinals up to type r.

• ordinal.card o: the cardinality of an ordinal o.

• ordinal.lift lifts an ordinal in universe u to an ordinal in universe max u v. For a version registering additionally that this is an initial segment embedding, see ordinal.lift.initial_seg. For a version regiserting that it is a principal segment embedding if u < v, see ordinal.lift.principal_seg.

• ordinal.omega is the first infinite ordinal. It is the order type of ℕ.

• 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₂. The main properties of addition (and the other operations on ordinals) are stated and proved in 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 ordinal o.

• ordinal.min: the minimal element of a nonempty indexed family of ordinals

• ordinal.omin : the minimal element of a nonempty set of ordinals

• cardinal.ord c: when c is a cardinal, ord c is 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 of r into s.
• r ≺i s: the type of principal segment embeddings of r into s.
• ω 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.

@[nolint]
structure initial_seg {α : Type u_4} {β : Type u_5} (r : α → α → Prop) (s : β → β → Prop) :
Type (max u_4 u_5)

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.

@[protected, instance]
def initial_seg.rel_embedding.has_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
has_coe s) (r ↪r s)
Equations
@[protected, instance]
def initial_seg.has_coe_to_fun {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
Equations
@[simp]
theorem initial_seg.coe_fn_mk {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (o : ∀ (a : α) (b : β), s b (f a)(∃ (a' : α), f a' = b)) :
@[simp]
theorem initial_seg.coe_fn_to_rel_embedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : s) :
@[simp]
theorem initial_seg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : s) :
theorem initial_seg.init' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : s) {a : α} {b : β} :
s b (f a)(∃ (a' : α), f a' = b)
theorem initial_seg.init_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : s) {a : α} {b : β} :
s b (f a) ∃ (a' : α), f a' = b r a' a
def initial_seg.of_iso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) :
s

An order isomorphism is an initial segment

Equations
@[protected]
def initial_seg.refl {α : Type u_1} (r : α → α → Prop) :
r

The identity function shows that ≼i is reflexive

Equations
@[protected]
def initial_seg.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : s) (g : t) :
t

Composition of functions shows that ≼i is transitive

Equations
@[simp]
theorem initial_seg.refl_apply {α : Type u_1} {r : α → α → Prop} (x : α) :
x = x
@[simp]
theorem initial_seg.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : s) (g : t) (a : α) :
(f.trans g) a = g (f a)
theorem initial_seg.unique_of_extensional {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] :
subsingleton s)
@[protected, instance]
def initial_seg.subsingleton {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] :
@[protected]
theorem initial_seg.eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f g : s) (a : α) :
f a = g a
theorem initial_seg.antisymm.aux {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ r] (f : s) (g : r) :
def initial_seg.antisymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : s) (g : r) :
r ≃r s

If we have order embeddings between α and β whose images are initial segments, and β is a well-order then α and β are order-isomorphic.

Equations
@[simp]
theorem initial_seg.antisymm_to_fun {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : s) (g : r) :
@[simp]
theorem initial_seg.antisymm_symm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] (f : s) (g : r) :
theorem initial_seg.eq_or_principal {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : s) :
∃ (b : β), ∀ (x : β), s x b ∃ (y : α), f y = x
def initial_seg.cod_restrict {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : set β) (f : s) (H : ∀ (a : α), f a p) :
(subrel s p)

Restrict the codomain of an initial segment

Equations
@[simp]
theorem initial_seg.cod_restrict_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : set β) (f : s) (H : ∀ (a : α), f a p) (a : α) :
H) a = f a, _⟩
def initial_seg.le_add {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) :
(sum.lex r s)

Initial segment embedding of an order r into the disjoint union of r and s.

Equations
@[simp]
theorem initial_seg.le_add_apply {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (a : α) :
s) a =

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

@[nolint]
structure principal_seg {α : Type u_4} {β : Type u_5} (r : α → α → Prop) (s : β → β → Prop) :
Type (max u_4 u_5)

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

@[protected, instance]
def principal_seg.rel_embedding.has_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
has_coe s) (r ↪r s)
Equations
@[protected, instance]
def principal_seg.has_coe_to_fun {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
Equations
@[simp]
theorem principal_seg.coe_fn_mk {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (t : β) (o : ∀ (b : β), s b t ∃ (a : α), f a = b) :
{to_rel_embedding := f, top := t, down := o} = f
@[simp]
theorem principal_seg.coe_fn_to_rel_embedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : s) :
@[simp]
theorem principal_seg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : s) :
theorem principal_seg.down' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : s) {b : β} :
s b f.top ∃ (a : α), f a = b
theorem principal_seg.lt_top {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : s) (a : α) :
s (f a) f.top
theorem principal_seg.init {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : s) {a : α} {b : β} (h : s b (f a)) :
∃ (a' : α), f a' = b
@[protected, instance]
def principal_seg.has_coe_initial_seg {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] :
has_coe s) s)

A principal segment is in particular an initial segment.

Equations
theorem principal_seg.coe_coe_fn' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : s) :
theorem principal_seg.init_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : s) {a : α} {b : β} :
s b (f a) ∃ (a' : α), f a' = b r a' a
theorem principal_seg.irrefl {α : Type u_1} (r : α → α → Prop) [ r] (f : r) :
def principal_seg.lt_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : s) (g : t) :

Composition of a principal segment with an initial segment, as a principal segment

Equations
@[simp]
theorem principal_seg.lt_le_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : s) (g : t) (a : α) :
(f.lt_le g) a = g (f a)
@[simp]
theorem principal_seg.lt_le_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : s) (g : t) :
(f.lt_le g).top = g f.top
@[protected]
def principal_seg.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [ t] (f : s) (g : t) :

Composition of two principal segments as a principal segment

Equations
@[simp]
theorem principal_seg.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [ t] (f : s) (g : t) (a : α) :
(f.trans g) a = g (f a)
@[simp]
theorem principal_seg.trans_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [ t] (f : s) (g : t) :
(f.trans g).top = g f.top
def principal_seg.equiv_lt {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≃r s) (g : t) :

Composition of an order isomorphism with a principal segment, as a principal segment

Equations
def principal_seg.lt_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : s) (g : s ≃r t) :

Composition of a principal segment with an order isomorphism, as a principal segment

Equations
@[simp]
theorem principal_seg.equiv_lt_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≃r s) (g : t) (a : α) :
a = g (f a)
@[simp]
theorem principal_seg.equiv_lt_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≃r s) (g : t) :
.top = g.top
@[protected, instance]
def principal_seg.subsingleton {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] :

Given a well order s, there is a most one principal segment embedding of r into s.

theorem principal_seg.top_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [ t] (e : r ≃r s) (f : t) (g : t) :
f.top = g.top
theorem principal_seg.top_lt_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [ t] (f : s) (g : t) (h : t) :
t h.top g.top
def principal_seg.of_element {α : Type u_1} (r : α → α → Prop) (a : α) :
principal_seg (subrel r {b : α | r b a}) r

Any element of a well order yields a principal segment

Equations
@[simp]
theorem principal_seg.of_element_apply {α : Type u_1} (r : α → α → Prop) (a : α) (b : {b : α | r b a}) :
b = b.val
@[simp]
theorem principal_seg.of_element_top {α : Type u_1} (r : α → α → Prop) (a : α) :
.top = a
def principal_seg.cod_restrict {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : set β) (f : s) (H : ∀ (a : α), f a p) (H₂ : f.top p) :
(subrel s p)

Restrict the codomain of a principal segment

Equations
@[simp]
theorem principal_seg.cod_restrict_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : set β) (f : s) (H : ∀ (a : α), f a p) (H₂ : f.top p) (a : α) :
H₂) a = f a, _⟩
@[simp]
theorem principal_seg.cod_restrict_top {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : set β) (f : s) (H : ∀ (a : α), f a p) (H₂ : f.top p) :
H₂).top = f.top, H₂⟩

### Properties of initial and principal segments #

def initial_seg.lt_or_eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : s) :
(r ≃r s)

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
theorem initial_seg.lt_or_eq_apply_left {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : s) (g : s) (a : α) :
g a = f a
theorem initial_seg.lt_or_eq_apply_right {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : s) (g : r ≃r s) (a : α) :
g a = f a
def initial_seg.le_lt {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [ s] [ t] (f : s) (g : t) :

Composition of an initial segment taking values in a well order and a principal segment.

Equations
@[simp]
theorem initial_seg.le_lt_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [ s] [ t] (f : s) (g : t) (a : α) :
(f.le_lt g) a = g (f a)
def rel_embedding.collapse_F {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : r ↪r s) (a : α) :
{b // ¬s (f a) b}

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 , _⟩)
theorem rel_embedding.collapse_F.lt {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : r ↪r s) {a a' : α} :
r a' as (f.collapse_F a').val (f.collapse_F a).val
theorem rel_embedding.collapse_F.not_lt {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : r ↪r s) (a : α) {b : β} (h : ∀ (a' : α), r a' as (f.collapse_F a').val b) :
¬s b (f.collapse_F a).val
def rel_embedding.collapse {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : r ↪r s) :
s

Construct an initial segment from an order embedding into a well order, by collapsing it to fill the gaps.

Equations
theorem rel_embedding.collapse_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ s] (f : r ↪r s) (a : α) :

### Well order on an arbitrary type #

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
@[protected, instance]
def well_ordering_rel.is_well_order {σ : Type u} :

### Definition of ordinals #

structure Well_order  :
Type (u+1)
• α : Type ?
• r : c.αc.α → Prop
• wo : c.r

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

@[protected, instance]
Equations
@[protected, instance]

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

Equations
def ordinal  :
Type (u+1)

ordinal.{u} is the type of well orders in Type u, up to order isomorphism.

Equations
def ordinal.type {α : Type u_1} (r : α → α → Prop) [wo : r] :

The order type of a well order is an ordinal.

Equations
def ordinal.typein {α : Type u_1} (r : α → α → Prop) [ r] (a : α) :

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

Equations
theorem ordinal.type_def {α : Type u_1} (r : α → α → Prop) [wo : r] :
{α := α, r := r, wo := wo} =
@[simp]
theorem ordinal.type_def' {α : Type u_1} (r : α → α → Prop) [ r] {wo : r} :
{α := α, r := r, wo := wo} =
theorem ordinal.type_eq {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] :
@[simp]
theorem ordinal.type_out (o : ordinal) :
= o
theorem ordinal.induction_on {C : ordinal → Prop} (o : ordinal) (H : ∀ (α : Type u_1) (r : α → α → Prop) [_inst_1 : r], C (ordinal.type r)) :
C o

### The order on ordinals #

@[protected]
def ordinal.le (a : ordinal) (b : ordinal) :
Prop

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 = (λ (_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 s)
@[protected, instance]
Equations
theorem ordinal.type_le {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] :
theorem ordinal.type_le' {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] :
def ordinal.lt (a : ordinal) (b : ordinal) :
Prop

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 = (λ (_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 s)
@[protected, instance]
Equations
@[simp]
theorem ordinal.type_lt {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] :
@[protected, instance]
Equations
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
• = (quotient.out α).cases_on (λ (α_1 : Type u_1) (r : α_1 → α_1 → Prop) (wo : r), (quotient.out β).cases_on (λ (α_2 : Type u_1) (r_1 : α_2 → α_2 → Prop) (wo_1 : r_1), classical.choice)) _
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
• = (quotient.out α).cases_on (λ (α_1 : Type u_1) (r : α_1 → α_1 → Prop) (wo : r), (quotient.out β).cases_on (λ (α_2 : Type u_1) (r_1 : α_2 → α_2 → Prop) (wo_1 : r_1), classical.choice)) _
def ordinal.rel_iso_out {α β : ordinal} (h : α = β) :

Given two ordinals α = β, then rel_iso_out α β is the order isomorphism between two model types for α and β.

Equations
• = (quotient.out α).cases_on (λ (α_1 : Type u_1) (r : α_1 → α_1 → Prop) (wo : r), (quotient.out β).cases_on (λ (α_2 : Type u_1) (r_1 : α_2 → α_2 → Prop) (wo_1 : r_1), _
theorem ordinal.typein_lt_type {α : Type u_1} (r : α → α → Prop) [ r] (a : α) :
@[simp]
theorem ordinal.typein_top {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] (f : s) :
@[simp]
theorem ordinal.typein_apply {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] (f : s) (a : α) :
(f a) =
@[simp]
theorem ordinal.typein_lt_typein {α : Type u_1} (r : α → α → Prop) [ r] {a b : α} :
< r a b
theorem ordinal.typein_surj {α : Type u_1} (r : α → α → Prop) [ r] {o : ordinal} (h : o < ) :
∃ (a : α), = o
theorem ordinal.typein_injective {α : Type u_1} (r : α → α → Prop) [ r] :
theorem ordinal.typein_inj {α : Type u_1} (r : α → α → Prop) [ r] {a b : α} :
= a = b

### Enumerating elements in a well-order with ordinals. #

def ordinal.enum {α : Type u_1} (r : α → α → Prop) [ 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} [ r] [ s] (f : r) {h : < } :
(ordinal.type s) h = f.top
@[simp]
theorem ordinal.enum_typein {α : Type u_1} (r : α → α → Prop) [ r] (a : α) {h : < } :
a) h = a
@[simp]
theorem ordinal.typein_enum {α : Type u_1} (r : α → α → Prop) [ r] {o : ordinal} (h : o < ) :
o h) = o
def ordinal.typein_iso {α : Type u_1} (r : α → α → Prop) [ r] :
r ≃r (λ (_x : ordinal), _x < ordinal.type r)

A well order r is order isomorphic to the set of ordinals strictly smaller than the ordinal version of r.

Equations
theorem ordinal.enum_lt {α : Type u_1} {r : α → α → Prop} [ r] {o₁ o₂ : ordinal} (h₁ : o₁ < ) (h₂ : o₂ < ) :
r o₁ h₁) o₂ h₂) o₁ < o₂
theorem ordinal.rel_iso_enum' {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] (f : r ≃r s) (o : ordinal) (hr : o < ) (hs : o < ) :
f o hr) = o hs
theorem ordinal.rel_iso_enum {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] (f : r ≃r s) (o : ordinal) (hr : o < ) :
f o hr) = o _
theorem ordinal.wf  :
@[protected, instance]
Equations
def ordinal.typein.principal_seg {α : Type u} (r : α → α → Prop) [ r] :

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

Equations
@[simp]
theorem ordinal.typein.principal_seg_coe {α : Type u_1} (r : α → α → Prop) [ r] :

### Cardinality of ordinals #

The cardinal of an ordinal is the cardinal of any set with that order type.

Equations
• o.card = (λ (_x : Well_order), ordinal.card._match_1 _x) ordinal.card._proof_1
• ordinal.card._match_1 {α := α, r := r, wo := _x} = # α
@[simp]
theorem ordinal.card_type {α : Type u_1} (r : α → α → Prop) [ r] :
theorem ordinal.card_typein {α : Type u_1} {r : α → α → Prop} [wo : r] (x : α) :
# {y // r y x} = x).card
theorem ordinal.card_le_card {o₁ o₂ : ordinal} :
o₁ o₂o₁.card o₂.card
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem ordinal.card_zero  :
0.card = 0
@[protected]
theorem ordinal.zero_le (o : ordinal) :
0 o
@[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, instance]
Equations
@[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
• o.lift = (λ (_x : Well_order), ordinal.lift._match_2 _x) ordinal.lift._proof_1
• ordinal.lift._match_2 {α := α, r := r, wo := wo} =
theorem ordinal.lift_type {α : Type u_1} (r : α → α → Prop) [ r] :
∃ (wo' : (equiv.ulift ⁻¹'o r)),
theorem ordinal.lift_id' (a : ordinal) :
a.lift = a
@[simp]
theorem ordinal.lift_id (a : ordinal) :
a.lift = a
@[simp]
theorem ordinal.lift_lift (a : ordinal) :
theorem ordinal.lift_type_le {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] :
theorem ordinal.lift_type_eq {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] :
theorem ordinal.lift_type_lt {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [ r] [ 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
@[simp]

### The first infinite ordinal omega#

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

Equations
@[simp]
theorem ordinal.lift_omega  :

### 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
@[simp]
theorem ordinal.card_add (o₁ o₂ : ordinal) :
(o₁ + o₂).card = o₁.card + o₂.card
@[simp]
theorem ordinal.card_nat (n : ) :
@[simp]
theorem ordinal.type_add {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [ r] [ s] :

The ordinal successor is the smallest ordinal larger than o. It is defined as o + 1.

Equations
theorem ordinal.succ_eq_add_one (o : ordinal) :
o.succ = o + 1
@[protected, instance]
Equations
theorem ordinal.add_le_add_left {a b : ordinal} :
a b∀ (c : ordinal), c + a c + b
theorem ordinal.le_add_right (a b : ordinal) :
a a + b
theorem ordinal.add_le_add_right {a b : ordinal} :
a b∀ (c : ordinal), a + c b + c
theorem ordinal.le_add_left (a b : ordinal) :
a b + a
theorem ordinal.lt_succ_self (o : ordinal) :
o < o.succ
theorem ordinal.succ_le {a b : ordinal} :
a.succ b a < b
theorem ordinal.le_total (a b : ordinal) :
a b b a
@[protected, instance]
Equations
@[protected, instance]
@[simp]
theorem ordinal.typein_le_typein {α : Type u_1} (r : α → α → Prop) [ r] {x x' : α} :
x' ¬r x' x
theorem ordinal.enum_le_enum {α : Type u_1} (r : α → α → Prop) [ r] {o o' : ordinal} (ho : o < ) (ho' : o' < ) :
¬r o' ho') o ho) o o'

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

Principal segment version of the lift operation on ordinals, embedding ordinal.{u} in ordinal.{v} as a principal segment when u < v.

Equations
@[simp]
@[simp]

### Minimum #

def ordinal.min {ι : Sort u_1} (I : nonempty ι) (f : ι → ordinal) :

The minimal element of a nonempty family of ordinals

Equations
• f = _
• _ = _
theorem ordinal.min_eq {ι : Sort u_1} (I : nonempty ι) (f : ι → ordinal) :
∃ (i : ι), f = f i
theorem ordinal.min_le {ι : Sort u_1} {I : nonempty ι} (f : ι → ordinal) (i : ι) :
f f i
theorem ordinal.le_min {ι : Sort u_1} {I : nonempty ι} {f : ι → ordinal} {a : ordinal} :
a f ∀ (i : ι), a f i
def ordinal.omin (S : set ordinal) (H : ∃ (x : ordinal), x S) :

The minimal element of a nonempty set of ordinals

Equations
• _ = _
theorem ordinal.omin_mem (S : set ordinal) (H : ∃ (x : ordinal), x S) :
H S
theorem ordinal.le_omin {S : set ordinal} {H : ∃ (x : ordinal), x S} {a : ordinal} :
a H ∀ (i : ordinal), i Sa i
theorem ordinal.omin_le {S : set ordinal} {H : ∃ (x : ordinal), x S} {i : ordinal} (h : i S) :
H i
@[simp]
theorem ordinal.lift_min {ι : Sort u_1} (I : nonempty ι) (f : ι → ordinal) :
f).lift =

### 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_1Type u_1 := λ (α : Type u_1), {r // r}, F : Type u_1ordinal := λ (α : Type u_1), (λ (i : ι α), {α := α, r := i.val, wo := _}) in F cardinal.ord._proof_3
theorem cardinal.ord_eq_min (α : Type u) :
(# α).ord = (λ (i : {r // r}), {α := α, r := i.val, wo := _})
theorem cardinal.ord_eq (α : Type u_1) :
∃ (r : α → α → Prop) [wo : r], (# α).ord =
theorem cardinal.ord_le_type {α : Type u_1} (r : α → α → Prop) [ r] :
(# α).ord
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
@[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.lift_ord (c : cardinal) :
theorem cardinal.card_typein_lt {α : Type u_1} (r : α → α → Prop) [ r] (x : α) (h : (# α).ord = ) :
x).card < # α

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

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
theorem cardinal.univ_id  :
@[simp]
@[simp]
theorem cardinal.lt_univ {c : cardinal} :
∃ (c' : cardinal), c = c'.lift
theorem cardinal.lt_univ' {c : cardinal} :
∃ (c' : cardinal), c = c'.lift
@[simp]