mathlib documentation

set_theory.ordinal.basic

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 #

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 #

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} :
Equations
@[protected, instance]
def initial_seg.has_coe_to_fun {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
has_coe_to_fun (initial_seg r s) (λ (_x : initial_seg r s), α → β)
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 : initial_seg r s) :
@[simp]
theorem initial_seg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : initial_seg r s) :
theorem initial_seg.init' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : initial_seg r 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 : initial_seg r 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) :

An order isomorphism is an initial segment

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

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 : initial_seg r s) (g : initial_seg s t) :

Composition of functions shows that ≼i is transitive

Equations
@[simp]
theorem initial_seg.refl_apply {α : Type u_1} {r : α → α → Prop} (x : α) :
@[simp]
theorem initial_seg.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : initial_seg r s) (g : initial_seg s 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} [is_extensional β s] :
@[protected, instance]
def initial_seg.subsingleton {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] :
@[protected]
theorem initial_seg.eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] (f g : initial_seg r s) (a : α) :
f a = g a
theorem initial_seg.antisymm.aux {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] (f : initial_seg r s) (g : initial_seg s r) :
def initial_seg.antisymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] (f : initial_seg r s) (g : initial_seg s 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} [is_well_order β s] (f : initial_seg r s) (g : initial_seg s r) :
@[simp]
theorem initial_seg.antisymm_symm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] (f : initial_seg r s) (g : initial_seg s r) :
theorem initial_seg.eq_or_principal {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] (f : initial_seg r s) :
function.surjective f ∃ (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 : initial_seg r s) (H : ∀ (a : α), f a 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 : initial_seg r s) (H : ∀ (a : α), f a p) (a : α) :
def initial_seg.le_add {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) :

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 : α) :

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} :
Equations
@[protected, instance]
def principal_seg.has_coe_to_fun {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
has_coe_to_fun (principal_seg r s) (λ (_x : principal_seg r s), α → β)
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 : principal_seg r s) :
@[simp]
theorem principal_seg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : principal_seg r s) :
theorem principal_seg.down' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : principal_seg r 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 : principal_seg r s) (a : α) :
s (f a) f.top
theorem principal_seg.init {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trans β s] (f : principal_seg r 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} [is_trans β 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} [is_trans β s] (f : principal_seg r s) :
theorem principal_seg.init_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trans β s] (f : principal_seg r s) {a : α} {b : β} :
s b (f a) ∃ (a' : α), f a' = b r a' a
theorem principal_seg.irrefl {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (f : principal_seg r r) :
def principal_seg.lt_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : principal_seg r s) (g : initial_seg s 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 : principal_seg r s) (g : initial_seg s 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 : principal_seg r s) (g : initial_seg s 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} [is_trans γ t] (f : principal_seg r s) (g : principal_seg s 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} [is_trans γ t] (f : principal_seg r s) (g : principal_seg s 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} [is_trans γ t] (f : principal_seg r s) (g : principal_seg s 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 : principal_seg s 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 : principal_seg r 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 : principal_seg s t) (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 : principal_seg s t) :
@[protected, instance]
def principal_seg.subsingleton {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β 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} [is_well_order γ t] (e : r ≃r s) (f : principal_seg r t) (g : principal_seg s 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} [is_well_order γ t] (f : principal_seg r s) (g : principal_seg s t) (h : principal_seg r 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}) :
@[simp]
theorem principal_seg.of_element_top {α : Type u_1} (r : α → α → Prop) (a : α) :
def principal_seg.cod_restrict {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : set β) (f : principal_seg r s) (H : ∀ (a : α), f a p) (H₂ : f.top 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 : principal_seg r s) (H : ∀ (a : α), f a p) (H₂ : f.top p) (a : α) :
(principal_seg.cod_restrict p f H H₂) a = f a, _⟩
@[simp]
theorem principal_seg.cod_restrict_top {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : set β) (f : principal_seg r s) (H : ∀ (a : α), f a p) (H₂ : f.top p) :
(principal_seg.cod_restrict p f H H₂).top = f.top, H₂⟩

Properties of initial and principal segments #

noncomputable def initial_seg.lt_or_eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] (f : initial_seg 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} [is_well_order β s] (f : initial_seg r s) (g : principal_seg r s) (a : α) :
g a = f a
theorem initial_seg.lt_or_eq_apply_right {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] (f : initial_seg r s) (g : r ≃r s) (a : α) :
g a = f a
noncomputable def initial_seg.le_lt {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [is_well_order β s] [is_trans γ t] (f : initial_seg r s) (g : principal_seg s 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} [is_well_order β s] [is_trans γ t] (f : initial_seg r s) (g : principal_seg s t) (a : α) :
(f.le_lt g) a = g (f a)
noncomputable def rel_embedding.collapse_F {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β 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
theorem rel_embedding.collapse_F.lt {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β 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} [is_well_order β 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
noncomputable def rel_embedding.collapse {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] (f : r ↪r 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} [is_well_order β s] (f : r ↪r s) (a : α) :

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
@[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.

@[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
@[protected, instance]
Equations
@[protected, instance]
noncomputable def α.linear_order (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
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
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_def' {α : Type u_1} (r : α → α → Prop) [is_well_order α r] {wo : is_well_order α r} :
{α := α, r := r, wo := wo} = ordinal.type r
theorem ordinal.type_eq {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
@[simp]
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]
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
@[protected, instance]
Equations
theorem ordinal.type_le {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
theorem ordinal.type_le' {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β 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
@[protected, instance]
Equations
@[simp]
theorem ordinal.type_lt_iff {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
@[protected, instance]
Equations
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
noncomputable 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
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] :
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) :
o < ordinal.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
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) :
noncomputable def ordinal.typein_iso {α : Type u_1} (r : α → α → Prop) [is_well_order α 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_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 < jp 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
@[simp]
theorem ordinal.typein.principal_seg_coe {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

Cardinality of ordinals #

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

Equations
@[simp]
theorem ordinal.card_type {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
theorem ordinal.card_typein {α : Type u_1} {r : α → α → Prop} [wo : is_well_order α r] (x : α) :
# {y // r y x} = (ordinal.typein r 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]
@[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
theorem ordinal.lift_type {α : Type u_1} (r : α → α → Prop) [is_well_order α 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} [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]
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) [is_well_order α r] [is_well_order β 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.le_add_right (a b : ordinal) :
a a + b
theorem ordinal.le_add_left (a b : ordinal) :
a b + a
theorem ordinal.lt_succ_self (o : ordinal) :
o < o.succ
theorem ordinal.succ_ne_self (o : ordinal) :
o.succ o
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]
noncomputable def ordinal.succ_order  :
Equations
theorem ordinal.lt_succ {a b : ordinal} :
a < b.succ a b
@[simp]
theorem ordinal.typein_le_typein {α : Type u_1} (r : α → α → Prop) [is_well_order α r] {x x' : α} :
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_le_enum' (a : ordinal) {o o' : ordinal} (ho : o < a) (ho' : o' < a) :
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).α) :
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.out_order_bot_of_pos {o : ordinal} (ho : 0 < o) :

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

Equations
@[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

Minimum #

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

The minimal element of a nonempty family of ordinals

Equations
theorem ordinal.min_eq {ι : Sort u_1} (I : nonempty ι) (f : ι → ordinal) :
∃ (i : ι), ordinal.min I f = f i
theorem ordinal.min_le {ι : Sort u_1} {I : nonempty ι} (f : ι → ordinal) (i : ι) :
theorem ordinal.le_min {ι : Sort u_1} {I : nonempty ι} {f : ι → ordinal} {a : ordinal} :
a ordinal.min I f ∀ (i : ι), a f i
@[simp]
theorem ordinal.lift_min {ι : Sort u_1} (I : nonempty ι) (f : ι → ordinal) :
@[simp]
theorem ordinal.bot_eq_zero  :
= 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]
@[simp]
theorem ordinal.Inf_empty  :

Representing a cardinal with an ordinal #

@[simp]
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_min (α : Type u) :
(# α).ord = ordinal.min _ (λ (i : {r // is_well_order α r}), {α := α, r := i.val, wo := _})
theorem cardinal.ord_eq (α : Type u_1) :
∃ (r : α → α → Prop) [wo : is_well_order α r], (# α).ord = ordinal.type r
theorem cardinal.ord_le_type {α : Type u_1} (r : α → α → Prop) [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
@[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 : (# α).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
theorem cardinal.lt_univ {c : cardinal} :
c < cardinal.univ ∃ (c' : cardinal), c = c'.lift
theorem cardinal.lt_univ' {c : cardinal} :
c < cardinal.univ ∃ (c' : cardinal), c = c'.lift