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.

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

source
@[protected, instance]
def initial_seg.rel_embedding.has_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
has_coe (initial_seg r s) (r ↪r s)
Equations
source
@[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
source
@[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)) :
⇑{to_rel_embedding := f, init := o} = ⇑f
source
@[simp]
theorem initial_seg.coe_fn_to_rel_embedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : initial_seg r s) :
⇑(f.to_rel_embedding) = ⇑f
source
@[simp]
theorem initial_seg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : initial_seg r s) :
⇑↑f = ⇑f
source
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)
source
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
source
def initial_seg.of_iso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) :
initial_seg r s

An order isomorphism is an initial segment

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

The identity function shows that ≼i is reflexive

Equations
source
@[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) :
initial_seg r t

Composition of functions shows that ≼i is transitive

Equations
source
@[simp]
theorem initial_seg.refl_apply {α : Type u_1} {r : α → α → Prop} (x : α) :
⇑(initial_seg.refl r) x = x
source
@[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)
source
theorem initial_seg.unique_of_extensional {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_extensional β s] :
well_founded r → subsingleton (initial_seg r s)
source
@[protected, instance]
def initial_seg.subsingleton {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] :
subsingleton (initial_seg r s)
source
@[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
source
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) :
function.left_inverse ⇑g ⇑f
source
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
source
@[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) :
⇑(f.antisymm g) = ⇑f
source
@[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) :
(f.antisymm g).symm = g.antisymm f
source
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
source
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) :
initial_seg r (subrel s p)

Restrict the codomain of an initial segment

Equations
source
@[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 : α) :
⇑(initial_seg.cod_restrict p f H) a = ⟨⇑f a, _⟩
source
def initial_seg.le_add {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) :
initial_seg r (sum.lex r s)

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

Equations
source
@[simp]
theorem initial_seg.le_add_apply {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (a : α) :
⇑(initial_seg.le_add r s) a = sum.inl 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.

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

source
@[protected, instance]
def principal_seg.rel_embedding.has_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
has_coe (principal_seg r s) (r ↪r s)
Equations
source
@[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
source
@[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
source
@[simp]
theorem principal_seg.coe_fn_to_rel_embedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : principal_seg r s) :
⇑(f.to_rel_embedding) = ⇑f
source
@[simp]
theorem principal_seg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : principal_seg r s) :
⇑↑f = ⇑f
source
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
source
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
source
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
source
@[protected, instance]
def principal_seg.has_coe_initial_seg {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trans β s] :
has_coe (principal_seg r s) (initial_seg r s)

A principal segment is in particular an initial segment.

Equations
source
theorem principal_seg.coe_coe_fn' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trans β s] (f : principal_seg r s) :
⇑↑f = ⇑f
source
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
source
theorem principal_seg.irrefl {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (f : principal_seg r r) :
false
source
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) :
principal_seg r t

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

Equations
source
@[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)
source
@[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
source
@[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) :
principal_seg r t

Composition of two principal segments as a principal segment

Equations
source
@[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)
source
@[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
source
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) :
principal_seg r t

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

Equations
source
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) :
principal_seg r t

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

Equations
source
@[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 : α) :
⇑(principal_seg.equiv_lt f g) a = ⇑g (⇑f a)
source
@[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) :
(principal_seg.equiv_lt f g).top = g.top
source
@[protected, instance]
def principal_seg.subsingleton {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] :
subsingleton (principal_seg r s)

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

source
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
source
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
source
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
source
@[simp]
theorem principal_seg.of_element_apply {α : Type u_1} (r : α → α → Prop) (a : α) (b : ↥{b : α | r b a}) :
⇑(principal_seg.of_element r a) b = b.val
source
@[simp]
theorem principal_seg.of_element_top {α : Type u_1} (r : α → α → Prop) (a : α) :
(principal_seg.of_element r a).top = a
source
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) :
principal_seg r (subrel s p)

Restrict the codomain of a principal segment

Equations
source
@[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, _⟩
source
@[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 #

source
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) :
principal_seg r 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
source
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
source
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
source
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) :
principal_seg r t

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

Equations
source
@[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)
source
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
source
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' a → s (f.collapse_F a').val (f.collapse_F a).val
source
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' a → s (f.collapse_F a').val b) :
¬s b (f.collapse_F a).val
source
noncomputable def rel_embedding.collapse {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] (f : r ↪r s) :
initial_seg r s

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

Equations
source
theorem rel_embedding.collapse_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] (f : r ↪r s) (a : α) :
⇑(f.collapse) a = (f.collapse_F a).val

Well order on an arbitrary type #

source
theorem nonempty_embedding_to_cardinal {σ : Type u} :
nonempty (σ ↪ cardinal)
source
noncomputable def embedding_to_cardinal {σ : Type u} :
σ ↪ cardinal

An embedding of any type to the set of cardinals.

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

Definition of ordinals #

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

source
@[protected, instance]
def Well_order.inhabited  :
inhabited Well_order
Equations
source
@[protected, instance]
def ordinal.is_equivalent  :
setoid Well_order

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

Equations
source
def ordinal  :
Type (u+1)

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

Equations
source
@[protected, instance]
def α.has_well_founded (o : ordinal) :
has_well_founded (quotient.out o).α
Equations
source
@[protected, instance]
noncomputable def α.linear_order (o : ordinal) :
linear_order (quotient.out o).α
Equations
source
@[protected, instance]
def has_lt.lt.is_well_order (o : ordinal) :
is_well_order (quotient.out o).α has_lt.lt
source
def ordinal.type {α : Type u_1} (r : α → α → Prop) [wo : is_well_order α r] :
ordinal

The order type of a well order is an ordinal.

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

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

Equations
source
theorem ordinal.type_def {α : Type u_1} (r : α → α → Prop) [wo : is_well_order α r] :
⟦{α := α, r := r, wo := wo}⟧ = ordinal.type r
source
@[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
source
theorem ordinal.type_eq {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
ordinal.type r = ordinal.type s ↔ nonempty (r ≃r s)
source
@[simp]
theorem ordinal.type_lt (o : ordinal) :
ordinal.type has_lt.lt = o
source
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 #

source
@[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
source
@[protected, instance]
def ordinal.has_le  :
has_le ordinal
Equations
source
theorem ordinal.type_le {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
ordinal.type r ≤ ordinal.type s ↔ nonempty (initial_seg r s)
source
theorem ordinal.type_le' {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
ordinal.type r ≤ ordinal.type s ↔ nonempty (r ↪r s)
source
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
source
@[protected, instance]
def ordinal.has_lt  :
has_lt ordinal
Equations
source
@[simp]
theorem ordinal.type_lt_iff {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
ordinal.type r < ordinal.type s ↔ nonempty (principal_seg r s)
source
@[protected, instance]
def ordinal.partial_order  :
partial_order ordinal
Equations
source
noncomputable def ordinal.initial_seg_out {α β : ordinal} (h : α ≤ β) :
initial_seg has_lt.lt has_lt.lt

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

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
source
noncomputable def ordinal.rel_iso_out {α β : ordinal} (h : α = β) :
has_lt.lt ≃r has_lt.lt

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

Equations
source
theorem ordinal.typein_lt_type {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (a : α) :
ordinal.typein r a < ordinal.type r
source
theorem ordinal.typein_lt_self {o : ordinal} (i : (quotient.out o).α) :
ordinal.typein has_lt.lt i < o
source
@[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) :
ordinal.typein s f.top = ordinal.type r
source
@[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 : α) :
ordinal.typein s (⇑f a) = ordinal.typein r a
source
@[simp]
theorem ordinal.typein_lt_typein {α : Type u_1} (r : α → α → Prop) [is_well_order α r] {a b : α} :
ordinal.typein r a < ordinal.typein r b ↔ r a b
source
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
source
theorem ordinal.typein_injective {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
function.injective (ordinal.typein r)
source
theorem ordinal.typein_inj {α : Type u_1} (r : α → α → Prop) [is_well_order α r] {a b : α} :
ordinal.typein r a = ordinal.typein r b ↔ a = b

Enumerating elements in a well-order with ordinals. #

source
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
source
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} :
ordinal.enum r (ordinal.type s) h = f.top
source
@[simp]
theorem ordinal.enum_typein {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (a : α) :
ordinal.enum r (ordinal.typein r a) _ = a
source
@[simp]
theorem ordinal.typein_enum {α : Type u_1} (r : α → α → Prop) [is_well_order α r] {o : ordinal} (h : o < ordinal.type r) :
ordinal.typein r (ordinal.enum r o h) = o
source
noncomputable def ordinal.typein_iso {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
r ≃r subrel has_lt.lt (λ (_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
source
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₂
source
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
source
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 _
source
theorem ordinal.wf  :
well_founded has_lt.lt
source
@[protected, instance]
def ordinal.has_well_founded  :
has_well_founded ordinal
Equations
source
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.

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

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

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

Cardinality of ordinals #

source
def ordinal.card (o : ordinal) :
cardinal

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

Equations
source
@[simp]
theorem ordinal.card_type {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
(ordinal.type r).card = # α
source
theorem ordinal.card_typein {α : Type u_1} {r : α → α → Prop} [wo : is_well_order α r] (x : α) :
# {y // r y x} = (ordinal.typein r x).card
source
theorem ordinal.card_le_card {o₁ o₂ : ordinal} :
o₁ ≤ o₂ → o₁.card ≤ o₂.card
source
@[protected, instance]
def ordinal.has_zero  :
has_zero ordinal
Equations
source
@[protected, instance]
def ordinal.inhabited  :
inhabited ordinal
Equations
source
theorem ordinal.zero_eq_type_empty  :
0 = ordinal.type empty_relation
source
@[simp]
theorem ordinal.card_zero  :
0.card = 0
source
@[protected]
theorem ordinal.zero_le (o : ordinal) :
0 ≤ o
source
@[protected, simp]
theorem ordinal.le_zero {o : ordinal} :
o ≤ 0 ↔ o = 0
source
@[protected]
theorem ordinal.pos_iff_ne_zero {o : ordinal} :
0 < o ↔ o ≠ 0
source
theorem ordinal.eq_zero_of_out_empty (o : ordinal) [h : is_empty (quotient.out o).α] :
o = 0
source
@[simp]
theorem ordinal.out_empty_iff_eq_zero {o : ordinal} :
is_empty (quotient.out o).α ↔ o = 0
source
@[simp]
theorem ordinal.out_nonempty_iff_ne_zero {o : ordinal} :
nonempty (quotient.out o).α ↔ o ≠ 0
source
@[protected, instance]
def ordinal.α.is_empty  :
is_empty (quotient.out 0).α
source
@[protected, instance]
def ordinal.has_one  :
has_one ordinal
Equations
source
theorem ordinal.one_eq_type_unit  :
1 = ordinal.type empty_relation
source
@[simp]
theorem ordinal.card_one  :
1.card = 1

Lifting ordinals to a higher universe #

source
def ordinal.lift (o : ordinal) :
ordinal

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
source
theorem ordinal.lift_type {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
∃ (wo' : is_well_order (ulift α) (⇑equiv.ulift ⁻¹'o r)), (ordinal.type r).lift = ordinal.type (⇑equiv.ulift ⁻¹'o r)
source
theorem ordinal.lift_umax  :
ordinal.lift = ordinal.lift
source
theorem ordinal.lift_id' (a : ordinal) :
a.lift = a
source
@[simp]
theorem ordinal.lift_id (a : ordinal) :
a.lift = a
source
@[simp]
theorem ordinal.lift_lift (a : ordinal) :
a.lift.lift = a.lift
source
theorem ordinal.lift_type_le {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
(ordinal.type r).lift ≤ (ordinal.type s).lift ↔ nonempty (initial_seg r s)
source
theorem ordinal.lift_type_eq {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
(ordinal.type r).lift = (ordinal.type s).lift ↔ nonempty (r ≃r s)
source
theorem ordinal.lift_type_lt {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
(ordinal.type r).lift < (ordinal.type s).lift ↔ nonempty (principal_seg r s)
source
@[simp]
theorem ordinal.lift_le {a b : ordinal} :
a.lift ≤ b.lift ↔ a ≤ b
source
@[simp]
theorem ordinal.lift_inj {a b : ordinal} :
a.lift = b.lift ↔ a = b
source
@[simp]
theorem ordinal.lift_lt {a b : ordinal} :
a.lift < b.lift ↔ a < b
source
@[simp]
theorem ordinal.lift_zero  :
0.lift = 0
source
theorem ordinal.zero_eq_lift_type_empty  :
0 = (ordinal.type empty_relation).lift
source
@[simp]
theorem ordinal.lift_one  :
1.lift = 1
source
theorem ordinal.one_eq_lift_type_unit  :
1 = (ordinal.type empty_relation).lift
source
@[simp]
theorem ordinal.lift_card (a : ordinal) :
a.card.lift = a.lift.card
source
theorem ordinal.lift_down' {a : cardinal} {b : ordinal} (h : b.card ≤ a.lift) :
∃ (a' : ordinal), a'.lift = b
source
theorem ordinal.lift_down {a : ordinal} {b : ordinal} (h : b ≤ a.lift) :
∃ (a' : ordinal), a'.lift = b
source
theorem ordinal.le_lift_iff {a : ordinal} {b : ordinal} :
b ≤ a.lift ↔ ∃ (a' : ordinal), a'.lift = b ∧ a' ≤ a
source
theorem ordinal.lt_lift_iff {a : ordinal} {b : ordinal} :
b < a.lift ↔ ∃ (a' : ordinal), a'.lift = b ∧ a' < a
source
def ordinal.lift.initial_seg  :
initial_seg has_lt.lt has_lt.lt

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

Equations
source
@[simp]
theorem ordinal.lift.initial_seg_coe  :
⇑ordinal.lift.initial_seg = ordinal.lift

The first infinite ordinal omega #

source
def ordinal.omega  :
ordinal

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

Equations
source
theorem ordinal.card_omega  :
ω.card = ω
source
@[simp]
theorem ordinal.lift_omega  :
ω.lift = ω

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.

source
@[protected, instance]
def ordinal.has_add  :
has_add ordinal

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
source
@[simp]
theorem ordinal.card_add (o₁ o₂ : ordinal) :
(o₁ + o₂).card = o₁.card + o₂.card
source
@[simp]
theorem ordinal.card_nat (n : ℕ) :
↑n.card = ↑n
source
@[simp]
theorem ordinal.type_add {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [is_well_order α r] [is_well_order β s] :
ordinal.type r + ordinal.type s = ordinal.type (sum.lex r s)
source
def ordinal.succ (o : ordinal) :
ordinal

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

Equations
source
theorem ordinal.succ_eq_add_one (o : ordinal) :
o.succ = o + 1
source
@[protected, instance]
def ordinal.add_monoid  :
add_monoid ordinal
Equations
source
@[protected, instance]
def ordinal.has_le.le.add_covariant_class  :
covariant_class ordinal ordinal has_add.add has_le.le
source
@[protected, instance]
def ordinal.has_le.le.add_swap_covariant_class  :
covariant_class ordinal ordinal (function.swap has_add.add) has_le.le
source
theorem ordinal.le_add_right (a b : ordinal) :
a ≤ a + b
source
theorem ordinal.le_add_left (a b : ordinal) :
a ≤ b + a
source
theorem ordinal.lt_succ_self (o : ordinal) :
o < o.succ
source
theorem ordinal.succ_ne_self (o : ordinal) :
o.succ ≠ o
source
theorem ordinal.succ_le {a b : ordinal} :
a.succ ≤ b ↔ a < b
source
theorem ordinal.le_total (a b : ordinal) :
a ≤ b ∨ b ≤ a
source
@[protected, instance]
noncomputable def ordinal.linear_order  :
linear_order ordinal
Equations
source
@[protected, instance]
def ordinal.has_lt.lt.is_well_order  :
is_well_order ordinal has_lt.lt
source
@[protected, instance]
noncomputable def ordinal.succ_order  :
succ_order ordinal
Equations
source
theorem ordinal.lt_succ {a b : ordinal} :
a < b.succ ↔ a ≤ b
source
@[simp]
theorem ordinal.typein_le_typein {α : Type u_1} (r : α → α → Prop) [is_well_order α r] {x x' : α} :
ordinal.typein r x ≤ ordinal.typein r x' ↔ ¬r x' x
source
@[simp]
theorem ordinal.typein_le_typein' (o : ordinal) {x x' : (quotient.out o).α} :
ordinal.typein has_lt.lt x ≤ ordinal.typein has_lt.lt x' ↔ x ≤ x'
source
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'
source
theorem ordinal.enum_le_enum' (a : ordinal) {o o' : ordinal} (ho : o < a) (ho' : o' < a) :
ordinal.enum has_lt.lt o _ ≤ ordinal.enum has_lt.lt o' _ ↔ o ≤ o'
source
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)
source
theorem ordinal.enum_zero_le' {o : ordinal} (h0 : 0 < o) (a : (quotient.out o).α) :
ordinal.enum has_lt.lt 0 _ ≤ a
source
theorem ordinal.le_enum_succ {o : ordinal} (a : (quotient.out o.succ).α) :
a ≤ ordinal.enum has_lt.lt o _
source
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₂
source
noncomputable def ordinal.out_order_bot_of_pos {o : ordinal} (ho : 0 < o) :
order_bot (quotient.out o).α

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

Equations
source
theorem ordinal.enum_zero_eq_bot {o : ordinal} (ho : 0 < o) :
ordinal.enum has_lt.lt 0 _ = ⊥
source
@[nolint]
def ordinal.univ  :
ordinal

univ.{u v} is the order type of the ordinals of Type u as a member of ordinal.{v} (when u < v). It is an inaccessible cardinal.

Equations
source
theorem ordinal.univ_id  :
ordinal.univ = ordinal.type has_lt.lt
source
@[simp]
theorem ordinal.lift_univ  :
ordinal.univ.lift = ordinal.univ
source
theorem ordinal.univ_umax  :
ordinal.univ = ordinal.univ
source
def ordinal.lift.principal_seg  :
principal_seg has_lt.lt has_lt.lt

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

Equations
source
@[simp]
theorem ordinal.lift.principal_seg_coe  :
⇑ordinal.lift.principal_seg = ordinal.lift
source
@[simp]
theorem ordinal.lift.principal_seg_top  :
ordinal.lift.principal_seg.top = ordinal.univ
source
theorem ordinal.lift.principal_seg_top'  :
ordinal.lift.principal_seg.top = ordinal.type has_lt.lt

Minimum #

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

The minimal element of a nonempty family of ordinals

Equations
source
theorem ordinal.min_eq {ι : Sort u_1} (I : nonempty ι) (f : ι → ordinal) :
∃ (i : ι), ordinal.min I f = f i
source
theorem ordinal.min_le {ι : Sort u_1} {I : nonempty ι} (f : ι → ordinal) (i : ι) :
ordinal.min I f ≤ f i
source
theorem ordinal.le_min {ι : Sort u_1} {I : nonempty ι} {f : ι → ordinal} {a : ordinal} :
a ≤ ordinal.min I f ↔ ∀ (i : ι), a ≤ f i
source
@[simp]
theorem ordinal.lift_min {ι : Sort u_1} (I : nonempty ι) (f : ι → ordinal) :
(ordinal.min I f).lift = ordinal.min I (ordinal.lift ∘ f)
source
@[protected, instance]
noncomputable def ordinal.conditionally_complete_linear_order_bot  :
conditionally_complete_linear_order_bot ordinal
Equations
source
@[simp]
theorem ordinal.bot_eq_zero  :
⊥ = 0
source
@[protected]
theorem ordinal.not_lt_zero (o : ordinal) :
¬o < 0
source
theorem ordinal.eq_zero_or_pos (a : ordinal) :
a = 0 ∨ 0 < a
source
@[protected, instance]
def ordinal.no_max_order  :
no_max_order ordinal
source
@[simp]
theorem ordinal.Inf_empty  :
Inf ∅ = 0

Representing a cardinal with an ordinal #

source
@[simp]
theorem cardinal.mk_ordinal_out (o : ordinal) :
# (quotient.out o).α = o.card
source
noncomputable def cardinal.ord (c : cardinal) :
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
source
theorem cardinal.ord_eq_min (α : Type u) :
(# α).ord = ordinal.min _ (λ (i : {r // is_well_order α r}), ⟦{α := α, r := i.val, wo := _}⟧)
source
theorem cardinal.ord_eq (α : Type u_1) :
∃ (r : α → α → Prop) [wo : is_well_order α r], (# α).ord = ordinal.type r
source
theorem cardinal.ord_le_type {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
(# α).ord ≤ ordinal.type r
source
theorem cardinal.ord_le {c : cardinal} {o : ordinal} :
c.ord ≤ o ↔ c ≤ o.card
source
theorem cardinal.lt_ord {c : cardinal} {o : ordinal} :
o < c.ord ↔ o.card < c
source
@[simp]
theorem cardinal.card_ord (c : cardinal) :
c.ord.card = c
source
theorem cardinal.ord_card_le (o : ordinal) :
o.card.ord ≤ o
source
theorem cardinal.lt_ord_succ_card (o : ordinal) :
o < o.card.succ.ord
source
@[simp]
theorem cardinal.ord_le_ord {c₁ c₂ : cardinal} :
c₁.ord ≤ c₂.ord ↔ c₁ ≤ c₂
source
@[simp]
theorem cardinal.ord_lt_ord {c₁ c₂ : cardinal} :
c₁.ord < c₂.ord ↔ c₁ < c₂
source
@[simp]
theorem cardinal.ord_zero  :
0.ord = 0
source
@[simp]
theorem cardinal.ord_nat (n : ℕ) :
↑n.ord = ↑n
source
@[simp]
theorem cardinal.ord_one  :
1.ord = 1
source
@[simp]
theorem cardinal.lift_ord (c : cardinal) :
c.ord.lift = c.lift.ord
source
theorem cardinal.mk_ord_out (c : cardinal) :
# (quotient.out c.ord).α = c
source
theorem cardinal.card_typein_lt {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (x : α) (h : (# α).ord = ordinal.type r) :
(ordinal.typein r x).card < # α
source
theorem cardinal.card_typein_out_lt (c : cardinal) (x : (quotient.out c.ord).α) :
(ordinal.typein has_lt.lt x).card < c
source
theorem cardinal.ord_injective  :
function.injective cardinal.ord
source
noncomputable def cardinal.ord.order_embedding  :
cardinal ↪o ordinal

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
source
@[simp]
theorem cardinal.ord.order_embedding_coe  :
⇑cardinal.ord.order_embedding = cardinal.ord
source
@[nolint]
def cardinal.univ  :
cardinal

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
source
theorem cardinal.univ_id  :
cardinal.univ = # ordinal
source
@[simp]
theorem cardinal.lift_univ  :
cardinal.univ.lift = cardinal.univ
source
theorem cardinal.univ_umax  :
cardinal.univ = cardinal.univ
source
theorem cardinal.lift_lt_univ (c : cardinal) :
c.lift < cardinal.univ
source
theorem cardinal.lift_lt_univ' (c : cardinal) :
c.lift < cardinal.univ
source
@[simp]
theorem cardinal.ord_univ  :
cardinal.univ.ord = ordinal.univ
source
theorem cardinal.lt_univ {c : cardinal} :
c < cardinal.univ ↔ ∃ (c' : cardinal), c = c'.lift
source
theorem cardinal.lt_univ' {c : cardinal} :
c < cardinal.univ ↔ ∃ (c' : cardinal), c = c'.lift
source
theorem cardinal.small_iff_lift_mk_lt_univ {α : Type u} :
small α ↔ (# α).lift < cardinal.univ
source
@[simp]
theorem ordinal.card_univ  :
ordinal.univ.card = cardinal.univ