mathlib3 documentation

set_theory.ordinal.basic

Ordinals #

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

Ordinals are defined as equivalences of well-ordered sets under order isomorphism. They are endowed with a total order, where an ordinal is smaller than another one if it embeds into it as an initial segment (or, equivalently, in any way). This total order is well founded.

Main definitions #

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 or ω is the order type of ℕ. This definition is universe polymorphic: ordinal.omega.{u} : ordinal.{u} (contrast with ℕ : Type, which lives in a specific universe). In some cases the universe level has to be given explicitly.
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.
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.

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 #

ω is a notation for the first infinite ordinal in the locale ordinal.

Well order on an arbitrary type #

theorem nonempty_embedding_to_cardinal {σ : Type u} :

nonempty (σ ↪ cardinal)

noncomputable def embedding_to_cardinal {σ : Type u} :

σ ↪ cardinal

An embedding of any type to the set of cardinals.

Equations

embedding_to_cardinal = classical.choice nonempty_embedding_to_cardinal

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

well_ordering_rel = ⇑embedding_to_cardinal ⁻¹'o has_lt.lt

Instances for well_ordering_rel

well_ordering_rel.is_well_order

@[protected, instance]

def well_ordering_rel.is_well_order {σ : Type u} :

is_well_order σ well_ordering_rel

@[protected, instance]

def is_well_order.subtype_nonempty {σ : Type u} :

nonempty {r // is_well_order σ r}

Definition of ordinals #

structure Well_order :

Type (u+1)

α : Type ?
r : self.α → self.α → Prop
wo : is_well_order self.α self.r

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

Instances for Well_order

Well_order.has_sizeof_inst
Well_order.inhabited
ordinal.is_equivalent

@[protected, instance]

def Well_order.inhabited :

inhabited Well_order

Equations

Well_order.inhabited = {default := {α := pempty, r := empty_relation pempty, wo := _}}

@[simp]

theorem Well_order.eta (o : Well_order) :

{α := o.α, r := o.r, wo := _} = o

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

ordinal.is_equivalent = {r := λ (_x : Well_order), ordinal.is_equivalent._match_2 _x, iseqv := ordinal.is_equivalent._proof_1}
ordinal.is_equivalent._match_2 {α := α, r := r, wo := wo} = λ (_x : Well_order), ordinal.is_equivalent._match_1 α r _x
ordinal.is_equivalent._match_1 α r {α := β, r := s, wo := wo'} = nonempty (r ≃r s)

def ordinal :

Type (u+1)

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

Equations

ordinal = quotient ordinal.is_equivalent

Instances for ordinal

@[protected, instance]

def has_well_founded_out (o : ordinal) :

has_well_founded (quotient.out o).α

Equations

has_well_founded_out o = {r := (quotient.out o).r, wf := _}

@[protected, instance]

noncomputable def linear_order_out (o : ordinal) :

linear_order (quotient.out o).α

Equations

linear_order_out o = is_well_order.linear_order (quotient.out o).r

@[protected, instance]

def is_well_order_out_lt (o : ordinal) :

is_well_order (quotient.out o).α has_lt.lt

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

The order type of a well order is an ordinal.

Equations

ordinal.type r = ⟦{α := α, r := r, wo := wo}⟧

@[protected, instance]

def ordinal.has_zero :

has_zero ordinal

Equations

ordinal.has_zero = {zero := ordinal.type empty_relation empty_relation.is_well_order}

@[protected, instance]

def ordinal.inhabited :

inhabited ordinal

Equations

ordinal.inhabited = {default := 0}

@[protected, instance]

def ordinal.has_one :

has_one ordinal

Equations

ordinal.has_one = {one := ordinal.type empty_relation empty_relation.is_well_order}

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

ordinal.typein r a = ordinal.type (subrel r {b : α | r b a})

@[simp]

theorem ordinal.type_def' (w : Well_order) :

⟦w⟧ = ordinal.type w.r

@[simp]

theorem ordinal.type_def {α : Type u_1} (r : α → α → Prop) [wo : is_well_order α r] :

⟦{α := α, r := r, wo := wo}⟧ = ordinal.type r

@[simp]

theorem ordinal.type_out (o : ordinal) :

ordinal.type (quotient.out o).r = o

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)

theorem rel_iso.ordinal_type_eq {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] (h : r ≃r s) :

ordinal.type r = ordinal.type s

@[simp]

theorem ordinal.type_lt (o : ordinal) :

ordinal.type has_lt.lt = o

theorem ordinal.type_eq_zero_of_empty {α : Type u_1} (r : α → α → Prop) [is_well_order α r] [is_empty α] :

ordinal.type r = 0

@[simp]

theorem ordinal.type_eq_zero_iff_is_empty {α : Type u_1} {r : α → α → Prop} [is_well_order α r] :

ordinal.type r = 0 ↔ is_empty α

theorem ordinal.type_ne_zero_iff_nonempty {α : Type u_1} {r : α → α → Prop} [is_well_order α r] :

ordinal.type r ≠ 0 ↔ nonempty α

theorem ordinal.type_ne_zero_of_nonempty {α : Type u_1} (r : α → α → Prop) [is_well_order α r] [h : nonempty α] :

ordinal.type r ≠ 0

theorem ordinal.type_pempty :

ordinal.type empty_relation = 0

theorem ordinal.type_empty :

ordinal.type empty_relation = 0

theorem ordinal.type_eq_one_of_unique {α : Type u_1} (r : α → α → Prop) [is_well_order α r] [unique α] :

ordinal.type r = 1

@[simp]

theorem ordinal.type_eq_one_iff_unique {α : Type u_1} {r : α → α → Prop} [is_well_order α r] :

ordinal.type r = 1 ↔ nonempty (unique α)

theorem ordinal.type_punit :

ordinal.type empty_relation = 1

theorem ordinal.type_unit :

ordinal.type empty_relation = 1

@[simp]

theorem ordinal.out_empty_iff_eq_zero {o : ordinal} :

is_empty (quotient.out o).α ↔ o = 0

theorem ordinal.eq_zero_of_out_empty (o : ordinal) [h : is_empty (quotient.out o).α] :

o = 0

@[protected, instance]

def ordinal.is_empty_out_zero :

is_empty (quotient.out 0).α

@[simp]

theorem ordinal.out_nonempty_iff_ne_zero {o : ordinal} :

nonempty (quotient.out o).α ↔ o ≠ 0

theorem ordinal.ne_zero_of_out_nonempty (o : ordinal) [h : nonempty (quotient.out o).α] :

o ≠ 0

@[protected]

theorem ordinal.one_ne_zero :

1 ≠ 0

@[protected, instance]

def ordinal.nontrivial :

nontrivial ordinal

@[simp]

theorem ordinal.type_preimage {α β : Type u} (r : α → α → Prop) [is_well_order α r] (f : β ≃ α) :

ordinal.type (⇑f ⁻¹'o r) = ordinal.type r

theorem ordinal.induction_on {C : ordinal → Prop} (o : ordinal) (H : ∀ (α : Type u_1) (r : α → α → Prop) [_inst_1 : is_well_order α r], C (ordinal.type r)) :

C o

The order on ordinals #

@[protected, instance]

def ordinal.partial_order :

partial_order ordinal

Equations

ordinal.partial_order = {le := λ (a b : ordinal), quotient.lift_on₂ a b (λ (_x : Well_order), ordinal.partial_order._match_2 _x) ordinal.partial_order._proof_1, lt := λ (a b : ordinal), quotient.lift_on₂ a b (λ (_x : Well_order), ordinal.partial_order._match_12 _x) ordinal.partial_order._proof_2, le_refl := ordinal.partial_order._proof_3, le_trans := ordinal.partial_order._proof_4, lt_iff_le_not_le := ordinal.partial_order._proof_5, le_antisymm := ordinal.partial_order._proof_6}
ordinal.partial_order._match_2 {α := α, r := r, wo := wo} = λ (_x : Well_order), ordinal.partial_order._match_1 α r _x
ordinal.partial_order._match_12 {α := α, r := r, wo := wo} = λ (_x : Well_order), ordinal.partial_order._match_11 α r _x
ordinal.partial_order._match_1 α r {α := β, r := s, wo := wo'} = nonempty (initial_seg r s)
ordinal.partial_order._match_11 α r {α := β, r := s, wo := wo'} = nonempty (principal_seg r s)

theorem ordinal.type_le_iff {α β : 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)

theorem ordinal.type_le_iff' {α β : 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)

theorem initial_seg.ordinal_type_le {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] (h : initial_seg r s) :

ordinal.type r ≤ ordinal.type s

theorem rel_embedding.ordinal_type_le {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] (h : r ↪r s) :

ordinal.type r ≤ ordinal.type s

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

theorem principal_seg.ordinal_type_lt {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] (h : principal_seg r s) :

ordinal.type r < ordinal.type s

@[protected]

theorem ordinal.zero_le (o : ordinal) :

0 ≤ o

@[protected, instance]

def ordinal.order_bot :

order_bot ordinal

Equations

ordinal.order_bot = {bot := 0, bot_le := ordinal.zero_le}

@[simp]

theorem ordinal.bot_eq_zero :

@[protected, simp]

theorem ordinal.le_zero {o : ordinal} :

o ≤ 0 ↔ o = 0

@[protected]

theorem ordinal.pos_iff_ne_zero {o : ordinal} :

0 < o ↔ o ≠ 0

@[protected]

theorem ordinal.not_lt_zero (o : ordinal) :

¬o < 0

theorem ordinal.eq_zero_or_pos (a : ordinal) :

a = 0 ∨ 0 < a

@[protected, instance]

def ordinal.zero_le_one_class :

zero_le_one_class ordinal

Equations

ordinal.zero_le_one_class = {zero_le_one := ordinal.zero_le_one_class._proof_1}

@[protected, instance]

def ordinal.ne_zero.one :

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

ordinal.initial_seg_out h = id ((quotient.out α).cases_on (λ (α_1 : Type u_1) (r : α_1 → α_1 → Prop) (wo : is_well_order α_1 r), (quotient.out β).cases_on (λ (α_2 : Type u_1) (r_1 : α_2 → α_2 → Prop) (wo_1 : is_well_order α_2 r_1), classical.choice)) _)

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

ordinal.principal_seg_out h = id ((quotient.out α).cases_on (λ (α_1 : Type u_1) (r : α_1 → α_1 → Prop) (wo : is_well_order α_1 r), (quotient.out β).cases_on (λ (α_2 : Type u_1) (r_1 : α_2 → α_2 → Prop) (wo_1 : is_well_order α_2 r_1), classical.choice)) _)

theorem ordinal.typein_lt_type {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (a : α) :

ordinal.typein r a < ordinal.type r

theorem ordinal.typein_lt_self {o : ordinal} (i : (quotient.out o).α) :

ordinal.typein has_lt.lt i < o

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

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

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

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] :

function.injective (ordinal.typein r)

@[simp]

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

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

ordinal.enum r o = quot.rec_on o (λ (_x : Well_order), ordinal.enum._match_1 r _x) _
ordinal.enum._match_1 r {α := β, r := s, wo := _x} = λ (h : quot.mk setoid.r {α := β, r := s, wo := _x} < ordinal.type r), (classical.choice h).top

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

@[simp]

theorem ordinal.enum_typein {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (a : α) :

ordinal.enum r (ordinal.typein r a) _ = a

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

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.lt_wf :

well_founded has_lt.lt

@[protected, instance]

def ordinal.has_well_founded :

has_well_founded ordinal

Equations

ordinal.has_well_founded = {r := has_lt.lt (preorder.to_has_lt ordinal), wf := ordinal.lt_wf}

theorem ordinal.induction {p : ordinal → Prop} (i : ordinal) (h : ∀ (j : ordinal), (∀ (k : ordinal), k < j → p k) → p j) :

p i

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

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

principal_seg r has_lt.lt

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

Equations

ordinal.typein.principal_seg r = {to_rel_embedding := rel_embedding.of_monotone (ordinal.typein r) _, top := ordinal.type r _inst_1, down' := _}

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

def ordinal.card :

ordinal → cardinal

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

Equations

ordinal.card = quotient.map Well_order.α ordinal.card._proof_1

@[simp]

theorem ordinal.card_type {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

(ordinal.type r).card = cardinal.mk α

@[simp]

theorem ordinal.card_typein {α : Type u_1} {r : α → α → Prop} [wo : is_well_order α r] (x : α) :

cardinal.mk {y // r y x} = (ordinal.typein r x).card

theorem ordinal.card_le_card {o₁ o₂ : ordinal} :

o₁ ≤ o₂ → o₁.card ≤ o₂.card

@[simp]

theorem ordinal.card_zero :

0.card = 0

@[simp]

theorem ordinal.card_eq_zero {o : ordinal} :

o.card = 0 ↔ o = 0

@[simp]

theorem ordinal.card_one :

1.card = 1

Lifting ordinals to a higher universe #

def ordinal.lift (o : 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

o.lift = quotient.lift_on o (λ (w : Well_order), ordinal.type (ulift.down ⁻¹'o w.r)) ordinal.lift._proof_2

@[simp]

theorem ordinal.type_ulift {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

ordinal.type (ulift.down ⁻¹'o r) = (ordinal.type r).lift

theorem rel_iso.ordinal_lift_type_eq {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] (f : r ≃r s) :

(ordinal.type r).lift = (ordinal.type s).lift

@[simp]

theorem ordinal.type_lift_preimage {α : Type u} {β : Type v} (r : α → α → Prop) [is_well_order α r] (f : β ≃ α) :

(ordinal.type (⇑f ⁻¹'o r)).lift = (ordinal.type r).lift

@[simp]

theorem ordinal.lift_umax :

ordinal.lift = ordinal.lift

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

@[simp]

theorem ordinal.lift_umax' :

ordinal.lift = ordinal.lift

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

@[simp]

theorem ordinal.lift_id' (a : ordinal) :

a.lift = a

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

@[simp]

theorem ordinal.lift_id (a : ordinal) :

a.lift = a

An ordinal lifted to the same universe equals itself.

@[simp]

theorem ordinal.lift_uzero (a : ordinal) :

a.lift = a

An ordinal lifted to the zero universe equals itself.

@[simp]

theorem ordinal.lift_lift (a : ordinal) :

a.lift.lift = a.lift

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)

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)

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)

@[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) :

a.card.lift = a.lift.card

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

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

ordinal.lift.initial_seg = {to_rel_embedding := {to_embedding := {to_fun := ordinal.lift, inj' := ordinal.lift.initial_seg._proof_1}, map_rel_iff' := ordinal.lift.initial_seg._proof_2}, init' := ordinal.lift.initial_seg._proof_3}

@[simp]

theorem ordinal.lift.initial_seg_coe :

⇑ordinal.lift.initial_seg = ordinal.lift

The first infinite ordinal `omega` #

def ordinal.omega :

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

Equations

ordinal.omega = (ordinal.type has_lt.lt).lift

@[simp]

theorem ordinal.type_nat_lt :

ordinal.type has_lt.lt = ordinal.omega

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

@[simp]

theorem ordinal.card_omega :

ordinal.omega.card = cardinal.aleph_0

@[simp]

theorem ordinal.lift_omega :

ordinal.omega.lift = ordinal.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]

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

ordinal.has_add = {add := λ (o₁ o₂ : ordinal), quotient.lift_on₂ o₁ o₂ (λ (_x : Well_order), ordinal.has_add._match_2 _x) ordinal.has_add._proof_1}
ordinal.has_add._match_2 {α := α, r := r, wo := wo} = λ (_x : Well_order), ordinal.has_add._match_1 α r wo _x
ordinal.has_add._match_1 α r wo {α := β, r := s, wo := wo'} = ordinal.type (sum.lex r s)

@[protected, instance]

def ordinal.add_monoid_with_one :

add_monoid_with_one ordinal

Equations

ordinal.add_monoid_with_one = {nat_cast := nat.unary_cast (add_zero_class.to_has_add ordinal), add := has_add.add ordinal.has_add, add_assoc := ordinal.add_monoid_with_one._proof_8, zero := 0, zero_add := ordinal.add_monoid_with_one._proof_9, add_zero := ordinal.add_monoid_with_one._proof_10, nsmul := add_monoid.nsmul._default 0 has_add.add ordinal.add_monoid_with_one._proof_4 ordinal.add_monoid_with_one._proof_5, nsmul_zero' := ordinal.add_monoid_with_one._proof_11, nsmul_succ' := ordinal.add_monoid_with_one._proof_12, one := 1, nat_cast_zero := ordinal.add_monoid_with_one._proof_13, nat_cast_succ := ordinal.add_monoid_with_one._proof_14}

@[simp]

theorem ordinal.card_add (o₁ o₂ : ordinal) :

(o₁ + o₂).card = o₁.card + o₂.card

@[simp]

theorem ordinal.type_sum_lex {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [is_well_order α r] [is_well_order β s] :

ordinal.type (sum.lex r s) = ordinal.type r + ordinal.type s

@[simp]

theorem ordinal.card_nat (n : ℕ) :

↑n.card = ↑n

@[protected, instance]

def ordinal.add_covariant_class_le :

covariant_class ordinal ordinal has_add.add has_le.le

@[protected, instance]

def ordinal.add_swap_covariant_class_le :

covariant_class ordinal ordinal (function.swap has_add.add) has_le.le

theorem ordinal.le_add_right (a b : ordinal) :

a ≤ a + b

theorem ordinal.le_add_left (a b : ordinal) :

a ≤ b + a

@[protected, instance]

noncomputable def ordinal.linear_order :

linear_order ordinal

Equations

ordinal.linear_order = {le := partial_order.le ordinal.partial_order, lt := partial_order.lt ordinal.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := ordinal.linear_order._proof_1, decidable_le := classical.dec_rel has_le.le, decidable_eq := decidable_eq_of_decidable_le (classical.dec_rel has_le.le), decidable_lt := decidable_lt_of_decidable_le (classical.dec_rel has_le.le), max := max_default (λ (a b : ordinal), classical.dec_rel has_le.le a b), max_def := ordinal.linear_order._proof_2, min := min_default (λ (a b : ordinal), classical.dec_rel has_le.le a b), min_def := ordinal.linear_order._proof_3}

@[protected, instance]

def ordinal.well_founded_lt :

well_founded_lt ordinal

@[protected, instance]

def ordinal.has_lt.lt.is_well_order :

is_well_order ordinal has_lt.lt

@[protected, instance]

noncomputable def ordinal.conditionally_complete_linear_order_bot :

conditionally_complete_linear_order_bot ordinal

Equations

ordinal.conditionally_complete_linear_order_bot = is_well_order.conditionally_complete_linear_order_bot ordinal

@[simp]

theorem ordinal.max_zero_left (a : ordinal) :

linear_order.max 0 a = a

@[simp]

theorem ordinal.max_zero_right (a : ordinal) :

linear_order.max a 0 = a

@[simp]

theorem ordinal.max_eq_zero {a b : ordinal} :

linear_order.max a b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem ordinal.Inf_empty :

has_Inf.Inf ∅ = 0

@[protected, instance]

def ordinal.no_max_order :

no_max_order ordinal

@[protected, instance]

noncomputable def ordinal.succ_order :

succ_order ordinal

Equations

ordinal.succ_order = succ_order.of_succ_le_iff (λ (o : ordinal), o + 1) ordinal.succ_order._proof_1

@[simp]

theorem ordinal.add_one_eq_succ (o : ordinal) :

o + 1 = order.succ o

@[simp]

theorem ordinal.succ_zero :

order.succ 0 = 1

@[simp]

theorem ordinal.succ_one :

order.succ 1 = 2

theorem ordinal.add_succ (o₁ o₂ : ordinal) :

o₁ + order.succ o₂ = order.succ (o₁ + o₂)

theorem ordinal.one_le_iff_pos {o : ordinal} :

1 ≤ o ↔ 0 < o

theorem ordinal.one_le_iff_ne_zero {o : ordinal} :

1 ≤ o ↔ o ≠ 0

theorem ordinal.succ_pos (o : ordinal) :

0 < order.succ o

theorem ordinal.succ_ne_zero (o : ordinal) :

order.succ o ≠ 0

theorem ordinal.lt_one_iff_zero {a : ordinal} :

a < 1 ↔ a = 0

theorem ordinal.le_one_iff {a : ordinal} :

a ≤ 1 ↔ a = 0 ∨ a = 1

@[simp]

theorem ordinal.card_succ (o : ordinal) :

(order.succ o).card = o.card + 1

theorem ordinal.nat_cast_succ (n : ℕ) :

↑(n.succ) = order.succ ↑n

@[protected, instance]

def ordinal.unique_Iio_one :

unique ↥(set.Iio 1)

Equations

ordinal.unique_Iio_one = {to_inhabited := {default := ⟨0, _⟩}, uniq := ordinal.unique_Iio_one._proof_1}

@[protected, instance]

noncomputable def ordinal.unique_out_one :

unique (quotient.out 1).α

Equations

ordinal.unique_out_one = {to_inhabited := {default := ordinal.enum has_lt.lt 0 ordinal.unique_out_one._proof_2}, uniq := ordinal.unique_out_one._proof_3}

theorem ordinal.one_out_eq (x : (quotient.out 1).α) :

x = ordinal.enum has_lt.lt 0 _

Extra properties of typein and enum #

@[simp]

theorem ordinal.typein_one_out (x : (quotient.out 1).α) :

ordinal.typein has_lt.lt x = 0

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

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

@[simp]

theorem ordinal.enum_le_enum {α : Type u_1} (r : α → α → Prop) [is_well_order α r] {o o' : ordinal} (ho : o < ordinal.type r) (ho' : o' < ordinal.type r) :

¬r (ordinal.enum r o' ho') (ordinal.enum r o ho) ↔ o ≤ o'

@[simp]

theorem ordinal.enum_le_enum' (a : ordinal) {o o' : ordinal} (ho : o < ordinal.type has_lt.lt) (ho' : o' < ordinal.type has_lt.lt) :

ordinal.enum has_lt.lt o ho ≤ ordinal.enum has_lt.lt o' ho' ↔ o ≤ o'

theorem ordinal.enum_zero_le {α : Type u_1} {r : α → α → Prop} [is_well_order α r] (h0 : 0 < ordinal.type r) (a : α) :

¬r a (ordinal.enum r 0 h0)

theorem ordinal.enum_zero_le' {o : ordinal} (h0 : 0 < o) (a : (quotient.out o).α) :

ordinal.enum has_lt.lt 0 _ ≤ a

theorem ordinal.le_enum_succ {o : ordinal} (a : (quotient.out (order.succ o)).α) :

a ≤ ordinal.enum has_lt.lt o _

@[simp]

theorem ordinal.enum_inj {α : Type u_1} {r : α → α → Prop} [is_well_order α r] {o₁ o₂ : ordinal} (h₁ : o₁ < ordinal.type r) (h₂ : o₂ < ordinal.type r) :

ordinal.enum r o₁ h₁ = ordinal.enum r o₂ h₂ ↔ o₁ = o₂

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

subrel has_lt.lt (λ (_x : ordinal), _x < ordinal.type r) ≃r r

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

Equations

ordinal.enum_iso r = {to_equiv := {to_fun := λ (x : ↥(λ (_x : ordinal), _x < ordinal.type r)), ordinal.enum r x.val _, inv_fun := λ (x : α), ⟨ordinal.typein r x, _⟩, left_inv := _, right_inv := _}, map_rel_iff' := _}

@[simp]

theorem ordinal.enum_iso_apply {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (x : ↥(λ (_x : ordinal), _x < ordinal.type r)) :

⇑(ordinal.enum_iso r) x = ordinal.enum r x.val _

@[simp]

theorem ordinal.enum_iso_symm_apply_coe {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (x : α) :

↑(⇑((ordinal.enum_iso r).symm) x) = ordinal.typein r x

@[simp]

theorem ordinal.enum_iso_out_apply (o : ordinal) (x : ↥(set.Iio o)) :

⇑(o.enum_iso_out) x = ordinal.enum has_lt.lt x.val _

@[simp]

theorem ordinal.enum_iso_out_symm_apply_coe (o : ordinal) (x : (quotient.out o).α) :

↑(⇑(rel_iso.symm o.enum_iso_out) x) = ordinal.typein has_lt.lt x

noncomputable def ordinal.enum_iso_out (o : ordinal) :

↥(set.Iio o) ≃o (quotient.out o).α

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

Equations

o.enum_iso_out = {to_equiv := {to_fun := λ (x : ↥(set.Iio o)), ordinal.enum has_lt.lt x.val _, inv_fun := λ (x : (quotient.out o).α), ⟨ordinal.typein has_lt.lt x, _⟩, left_inv := _, right_inv := _}, map_rel_iff' := _}

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

ordinal.out_order_bot_of_pos ho = {bot := (λ (_x : Well_order), ordinal.enum._match_1 has_lt.lt _x) {α := pempty, r := empty_relation pempty, wo := _} _, bot_le := _}

theorem ordinal.enum_zero_eq_bot {o : ordinal} (ho : 0 < o) :

ordinal.enum has_lt.lt 0 _ = ⊥

Universal ordinal #

@[nolint]

def ordinal.univ :

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

ordinal.univ = (ordinal.type has_lt.lt).lift

theorem ordinal.univ_id :

ordinal.univ = ordinal.type has_lt.lt

@[simp]

theorem ordinal.lift_univ :

ordinal.univ.lift = ordinal.univ

theorem ordinal.univ_umax :

ordinal.univ = ordinal.univ

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

ordinal.lift.principal_seg = {to_rel_embedding := ↑ordinal.lift.initial_seg, top := ordinal.univ, down' := ordinal.lift.principal_seg._proof_1}

@[simp]

theorem ordinal.lift.principal_seg_coe :

⇑ordinal.lift.principal_seg = ordinal.lift

@[simp]

theorem ordinal.lift.principal_seg_top :

ordinal.lift.principal_seg.top = ordinal.univ

theorem ordinal.lift.principal_seg_top' :

ordinal.lift.principal_seg.top = ordinal.type has_lt.lt

Representing a cardinal with an ordinal #

@[simp]

theorem cardinal.mk_ordinal_out (o : ordinal) :

cardinal.mk (quotient.out o).α = o.card

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

c.ord = let F : Type u → ordinal := λ (α : Type u), ⨅ (r : {r // is_well_order α r}), ordinal.type r.val in quot.lift_on c F cardinal.ord._proof_2

theorem cardinal.ord_eq_Inf (α : Type u) :

(cardinal.mk α).ord = ⨅ (r : {r // is_well_order α r}), ordinal.type r.val

theorem cardinal.ord_eq (α : Type u_1) :

∃ (r : α → α → Prop) [wo : is_well_order α r], (cardinal.mk α).ord = ordinal.type r

theorem cardinal.ord_le_type {α : Type u_1} (r : α → α → Prop) [h : is_well_order α r] :

(cardinal.mk α).ord ≤ ordinal.type r

theorem cardinal.ord_le {c : cardinal} {o : ordinal} :

c.ord ≤ o ↔ c ≤ o.card

theorem cardinal.gc_ord_card :

galois_connection cardinal.ord ordinal.card

theorem cardinal.lt_ord {c : cardinal} {o : ordinal} :

o < c.ord ↔ o.card < c

@[simp]

theorem cardinal.card_ord (c : cardinal) :

noncomputable def cardinal.gci_ord_card :

galois_coinsertion cardinal.ord ordinal.card

Galois coinsertion between cardinal.ord and ordinal.card.

Equations

cardinal.gci_ord_card = cardinal.gc_ord_card.to_galois_coinsertion cardinal.gci_ord_card._proof_1

theorem cardinal.ord_card_le (o : ordinal) :

o.card.ord ≤ o

theorem cardinal.lt_ord_succ_card (o : ordinal) :

o < (order.succ o.card).ord

theorem cardinal.ord_strict_mono :

strict_mono cardinal.ord

theorem cardinal.ord_mono :

monotone cardinal.ord

@[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 : ℕ) :

↑n.ord = ↑n

@[simp]

theorem cardinal.ord_one :

1.ord = 1

@[simp]

theorem cardinal.lift_ord (c : cardinal) :

c.ord.lift = c.lift.ord

theorem cardinal.mk_ord_out (c : cardinal) :

cardinal.mk (quotient.out c.ord).α = c

theorem cardinal.card_typein_lt {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (x : α) (h : (cardinal.mk α).ord = ordinal.type r) :

(ordinal.typein r x).card < cardinal.mk α

theorem cardinal.card_typein_out_lt (c : cardinal) (x : (quotient.out c.ord).α) :

(ordinal.typein has_lt.lt x).card < c

theorem cardinal.ord_injective :

function.injective cardinal.ord

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

cardinal.ord.order_embedding = (rel_embedding.of_monotone cardinal.ord cardinal.ord.order_embedding._proof_1).order_embedding_of_lt_embedding

@[simp]

theorem cardinal.ord.order_embedding_coe :

⇑cardinal.ord.order_embedding = cardinal.ord

@[nolint]

def cardinal.univ :

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

cardinal.univ = (cardinal.mk ordinal).lift

theorem cardinal.univ_id :

cardinal.univ = cardinal.mk ordinal

@[simp]

theorem cardinal.lift_univ :

cardinal.univ.lift = cardinal.univ

theorem cardinal.univ_umax :

cardinal.univ = cardinal.univ

theorem cardinal.lift_lt_univ (c : cardinal) :

c.lift < cardinal.univ

theorem cardinal.lift_lt_univ' (c : cardinal) :

c.lift < cardinal.univ

@[simp]

theorem cardinal.ord_univ :

cardinal.univ.ord = ordinal.univ

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

theorem cardinal.small_iff_lift_mk_lt_univ {α : Type u} :

small α ↔ (cardinal.mk α).lift < cardinal.univ

@[simp]

theorem ordinal.card_univ :

ordinal.univ.card = cardinal.univ

@[simp]

theorem ordinal.nat_le_card {o : ordinal} {n : ℕ} :

↑n ≤ o.card ↔ ↑n ≤ o

@[simp]

theorem ordinal.nat_lt_card {o : ordinal} {n : ℕ} :

↑n < o.card ↔ ↑n < o

@[simp]

theorem ordinal.card_lt_nat {o : ordinal} {n : ℕ} :

o.card < ↑n ↔ o < ↑n

@[simp]

theorem ordinal.card_le_nat {o : ordinal} {n : ℕ} :

o.card ≤ ↑n ↔ o ≤ ↑n

@[simp]

theorem ordinal.card_eq_nat {o : ordinal} {n : ℕ} :

o.card = ↑n ↔ o = ↑n

@[simp]

theorem ordinal.type_fintype {α : Type u_1} (r : α → α → Prop) [is_well_order α r] [fintype α] :

ordinal.type r = ↑(fintype.card α)

theorem ordinal.type_fin (n : ℕ) :

ordinal.type has_lt.lt = ↑n