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 #

• 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.initialSeg. For a version registering that it is a principal segment embedding if u < v, see Ordinal.lift.principalSeg.

• 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 Mathlib/SetTheory/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 #

def embeddingToCardinal {σ : Type u} :

An embedding of any type to the set of cardinals.

Equations
• embeddingToCardinal =
Instances For
def WellOrderingRel {σ : Type u} :
σσProp

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

Equations
Instances For
instance WellOrderingRel.isWellOrder {σ : Type u} :
IsWellOrder σ WellOrderingRel
Equations
• =
instance IsWellOrder.subtype_nonempty {σ : Type u} :
Nonempty { r : σσProp // }
Equations
• =

Definition of ordinals #

structure WellOrder :
Type (u + 1)

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

• α : Type u

The underlying type of the order.

• r : selfselfProp

The underlying relation of the order.

• wo : IsWellOrder self self.r

The proposition that r is a well-ordering for α.

Instances For
theorem WellOrder.wo (self : WellOrder) :
IsWellOrder self self.r

The proposition that r is a well-ordering for α.

Equations
@[simp]
theorem WellOrder.eta (o : WellOrder) :
{ α := o, r := o.r, wo := } = o

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

Equations
• One or more equations did not get rendered due to their size.
def Ordinal :
Type (u + 1)

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

Equations
Instances For
Equations
instance isWellOrder_out_lt (o : Ordinal.{u_3}) :
IsWellOrder (Quotient.out o) fun (x x_1 : (Quotient.out o)) => x < x_1
Equations
• =

Basic properties of the order type #

def Ordinal.type {α : Type u} (r : ααProp) [wo : ] :

The order type of a well order is an ordinal.

Equations
• = { α := α, r := r, wo := wo }
Instances For
instance Ordinal.zero :
Equations
Equations
instance Ordinal.one :
Equations
def Ordinal.typein {α : Type u} (r : ααProp) [] (a : α) :

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

Equations
Instances For
@[simp]
theorem Ordinal.type_def' (w : WellOrder) :
w = Ordinal.type w.r
@[simp]
theorem Ordinal.type_def {α : Type u} (r : ααProp) [wo : ] :
{ α := α, r := r, wo := wo } =
theorem Ordinal.type_eq {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [] [] :
theorem RelIso.ordinal_type_eq {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [] [] (h : r ≃r s) :
@[simp]
theorem Ordinal.type_lt (o : Ordinal.{u_3}) :
(Ordinal.type fun (x x_1 : (Quotient.out o)) => x < x_1) = o
theorem Ordinal.type_eq_zero_of_empty {α : Type u} (r : ααProp) [] [] :
@[simp]
theorem Ordinal.type_eq_zero_iff_isEmpty {α : Type u} {r : ααProp} [] :
theorem Ordinal.type_ne_zero_iff_nonempty {α : Type u} {r : ααProp} [] :
theorem Ordinal.type_ne_zero_of_nonempty {α : Type u} (r : ααProp) [] [h : ] :
theorem Ordinal.type_pEmpty :
Ordinal.type EmptyRelation = 0
theorem Ordinal.type_empty :
Ordinal.type EmptyRelation = 0
theorem Ordinal.type_eq_one_of_unique {α : Type u} (r : ααProp) [] [] :
@[simp]
theorem Ordinal.type_eq_one_iff_unique {α : Type u} {r : ααProp} [] :
theorem Ordinal.type_pUnit :
Ordinal.type EmptyRelation = 1
theorem Ordinal.type_unit :
Ordinal.type EmptyRelation = 1
Equations
theorem Ordinal.type_preimage {α : Type u} {β : Type u} (r : ααProp) [] (f : β α) :
@[simp]
theorem Ordinal.type_preimage_aux {α : Type u} {β : Type u} (r : ααProp) [] (f : β α) :
(Ordinal.type fun (x y : β) => r (f x) (f y)) =
theorem Ordinal.inductionOn {C : } (o : Ordinal.{u_3}) (H : ∀ (α : Type u_3) (r : ααProp) [inst : ], C (Ordinal.type r)) :
C o

The order on ordinals #

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

• 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
theorem Ordinal.type_le_iff {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [] [] :
theorem Ordinal.type_le_iff' {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [] [] :
theorem InitialSeg.ordinal_type_le {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [] [] (h : r ≼i s) :
theorem RelEmbedding.ordinal_type_le {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [] [] (h : r ↪r s) :
@[simp]
theorem Ordinal.type_lt_iff {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [] [] :
theorem PrincipalSeg.ordinal_type_lt {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [] [] (h : r ≺i s) :
@[simp]
theorem Ordinal.zero_le (o : Ordinal.{u_3}) :
0 o
instance Ordinal.orderBot :
Equations
@[simp]
@[simp]
theorem Ordinal.le_zero {o : Ordinal.{u_3}} :
o 0 o = 0
Equations
Equations
def Ordinal.initialSegOut {α : Ordinal.{u_3}} {β : Ordinal.{u_3}} (h : α β) :
(fun (x x_1 : (Quotient.out α)) => x < x_1) ≼i fun (x x_1 : (Quotient.out β)) => x < x_1

Given two ordinals α ≤ β, then initialSegOut α β is the initial segment embedding of α to β, as map from a model type for α to a model type for β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Ordinal.principalSegOut {α : Ordinal.{u_3}} {β : Ordinal.{u_3}} (h : α < β) :
(fun (x x_1 : (Quotient.out α)) => x < x_1) ≺i fun (x x_1 : (Quotient.out β)) => x < x_1

Given two ordinals α < β, then principalSegOut α β is the principal segment embedding of α to β, as map from a model type for α to a model type for β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Ordinal.typein_lt_type {α : Type u} (r : ααProp) [] (a : α) :
theorem Ordinal.typein_lt_self {o : Ordinal.{u_3}} (i : (Quotient.out o)) :
Ordinal.typein (fun (x x_1 : (Quotient.out o)) => x < x_1) i < o
@[simp]
theorem Ordinal.typein_top {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [] [] (f : r ≺i s) :
Ordinal.typein s f.top =
@[simp]
theorem Ordinal.typein_apply {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [] [] (f : r ≼i s) (a : α) :
Ordinal.typein s (f a) =
@[simp]
theorem Ordinal.typein_lt_typein {α : Type u} (r : ααProp) [] {a : α} {b : α} :
< r a b
theorem Ordinal.typein_surj {α : Type u} (r : ααProp) [] {o : Ordinal.{u}} (h : ) :
∃ (a : α), = o
theorem Ordinal.typein_injective {α : Type u} (r : ααProp) [] :
@[simp]
theorem Ordinal.typein_inj {α : Type u} (r : ααProp) [] {a : α} {b : α} :
= a = b
def Ordinal.typein.principalSeg {α : Type u} (r : ααProp) [] :
r ≺i fun (x x_1 : Ordinal.{u}) => x < x_1

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

Equations
• = { toFun := , inj' := , map_rel_iff' := , top := , down' := }
Instances For
@[simp]
theorem Ordinal.typein.principalSeg_coe {α : Type u} (r : ααProp) [] :
.toRelEmbedding =

Enumerating elements in a well-order with ordinals. #

def Ordinal.enum {α : Type u} (r : ααProp) [] (o : Ordinal.{u}) (h : ) :
α

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
Instances For
@[simp]
theorem Ordinal.typein_enum {α : Type u} (r : ααProp) [] {o : Ordinal.{u}} (h : ) :
theorem Ordinal.enum_type {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [] [] (f : s ≺i r) {h : } :
@[simp]
theorem Ordinal.enum_typein {α : Type u} (r : ααProp) [] (a : α) :
theorem Ordinal.enum_lt_enum {α : Type u} {r : ααProp} [] {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (h₁ : o₁ < ) (h₂ : o₂ < ) :
r (Ordinal.enum r o₁ h₁) (Ordinal.enum r o₂ h₂) o₁ < o₂
theorem Ordinal.relIso_enum' {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} [] [] (f : r ≃r s) (o : Ordinal.{u}) (hr : ) (hs : ) :
f (Ordinal.enum r o hr) = Ordinal.enum s o hs
theorem Ordinal.relIso_enum {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} [] [] (f : r ≃r s) (o : Ordinal.{u}) (hr : ) :
f (Ordinal.enum r o hr) = Ordinal.enum s o
theorem Ordinal.lt_wf :
WellFounded fun (x x_1 : Ordinal.{u_3}) => x < x_1
Equations
theorem Ordinal.induction {p : } (i : Ordinal.{u}) (h : ∀ (j : Ordinal.{u}), (∀ 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 | h i IH => ?_.

Cardinality of ordinals #

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

Equations
Instances For
@[simp]
theorem Ordinal.card_type {α : Type u} (r : ααProp) [] :
(Ordinal.type r).card =
@[simp]
theorem Ordinal.card_typein {α : Type u} {r : ααProp} [] (x : α) :
Cardinal.mk { y : α // r y x } = (Ordinal.typein r x).card
theorem Ordinal.card_le_card {o₁ : Ordinal.{u_3}} {o₂ : Ordinal.{u_3}} :
o₁ o₂o₁.card o₂.card
@[simp]
@[simp]

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

Equations
Instances For
theorem Ordinal.type_uLift {α : Type u} (r : ααProp) [] :
Ordinal.type (ULift.down ⁻¹'o r) =
@[simp]
theorem Ordinal.type_uLift_aux {α : Type u} (r : ααProp) [] :
(Ordinal.type fun (x y : ) => r x.down y.down) =
theorem RelIso.ordinal_lift_type_eq {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [] [] (f : r ≃r s) :
=
theorem Ordinal.type_lift_preimage {α : Type u} {β : Type v} (r : ααProp) [] (f : β α) :
@[simp]
theorem Ordinal.type_lift_preimage_aux {α : Type u} {β : Type v} (r : ααProp) [] (f : β α) :
Ordinal.lift.{u, v} (Ordinal.type fun (x y : β) => r (f x) (f y)) =

lift.{max u v, u} equals lift.{v, u}.

lift.{max v u, u} equals lift.{v, u}.

theorem Ordinal.lift_id' :
= a

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

@[simp]
theorem Ordinal.lift_id (a : Ordinal.{u}) :
= a

An ordinal lifted to the same universe equals itself.

@[simp]
theorem Ordinal.lift_uzero (a : Ordinal.{u}) :
= a

An ordinal lifted to the zero universe equals itself.

@[simp]
theorem Ordinal.lift_type_le {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [] [] :
theorem Ordinal.lift_type_eq {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [] [] :
theorem Ordinal.lift_type_lt {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [] [] :
@[simp]
theorem Ordinal.lift_le {a : Ordinal.{v}} {b : Ordinal.{v}} :
a b
@[simp]
theorem Ordinal.lift_inj {a : Ordinal.{v}} {b : Ordinal.{v}} :
= a = b
@[simp]
theorem Ordinal.lift_lt {a : Ordinal.{v}} {b : Ordinal.{v}} :
< a < b
@[simp]
theorem Ordinal.lift_zero :
= 0
@[simp]
theorem Ordinal.lift_one :
= 1
@[simp]
theorem Ordinal.lift_down' {a : Cardinal.{u}} {b : Ordinal.{max u v} } (h : b.card ) :
∃ (a' : Ordinal.{u}), = b
theorem Ordinal.lift_down {a : Ordinal.{u}} {b : Ordinal.{max u v} } (h : b ) :
∃ (a' : Ordinal.{u}), = b
theorem Ordinal.lt_lift_iff {a : Ordinal.{u}} {b : Ordinal.{max u v} } :
b < ∃ (a' : Ordinal.{u}), = b a' < a
def Ordinal.lift.initialSeg :
(fun (x x_1 : Ordinal.{u}) => x < x_1) ≼i fun (x x_1 : Ordinal.{max u v} ) => x < x_1

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

Equations
Instances For
@[simp]

The first infinite ordinal omega#

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

Equations
Instances For

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

Equations
Instances For
@[simp]
theorem Ordinal.type_nat_lt :
(Ordinal.type fun (x x_1 : ) => x < x_1) = Ordinal.omega

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

@[simp]
@[simp]

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 Mathlib/SetTheory/Ordinal/Arithmetic.lean.

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
• One or more equations did not get rendered due to their size.
@[simp]
theorem Ordinal.card_add (o₁ : Ordinal.{u_3}) (o₂ : Ordinal.{u_3}) :
(o₁ + o₂).card = o₁.card + o₂.card
@[simp]
theorem Ordinal.type_sum_lex {α : Type u} {β : Type u} (r : ααProp) (s : ββProp) [] [] :
@[simp]
theorem Ordinal.card_nat (n : ) :
(↑n).card = n
@[simp]
theorem Ordinal.card_ofNat (n : ) [n.AtLeastTwo] :
(OfNat.ofNat n).card =
CovariantClass Ordinal.{u} Ordinal.{u} (fun (x x_1 : Ordinal.{u}) => x + x_1) fun (x x_1 : Ordinal.{u}) => x x_1
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
@[simp]
theorem Ordinal.max_eq_zero {a : Ordinal.{u_3}} {b : Ordinal.{u_3}} :
max a b = 0 a = 0 b = 0
@[simp]
theorem Ordinal.sInf_empty :
= 0

Successor order properties #

Equations
@[simp]
@[simp]
theorem Ordinal.succ_zero :
= 1
@[simp]
theorem Ordinal.succ_one :
= 2
theorem Ordinal.add_succ (o₁ : Ordinal.{u_3}) (o₂ : Ordinal.{u_3}) :
o₁ + = Order.succ (o₁ + o₂)
@[simp]
theorem Ordinal.le_one_iff {a : Ordinal.{u_3}} :
a 1 a = 0 a = 1
@[simp]
theorem Ordinal.card_succ (o : Ordinal.{u_3}) :
(Order.succ o).card = o.card + 1
theorem Ordinal.natCast_succ (n : ) :
n.succ =
@[deprecated Ordinal.natCast_succ]
theorem Ordinal.nat_cast_succ (n : ) :
n.succ =

Alias of Ordinal.natCast_succ.

theorem Ordinal.one_out_eq (x : (Quotient.out 1)) :
x = Ordinal.enum (fun (x x_1 : (Quotient.out 1)) => x < x_1) 0

Extra properties of typein and enum #

@[simp]
theorem Ordinal.typein_one_out (x : (Quotient.out 1)) :
Ordinal.typein (fun (x x_1 : (Quotient.out 1)) => x < x_1) x = 0
@[simp]
theorem Ordinal.typein_le_typein {α : Type u} (r : ααProp) [] {x : α} {x' : α} :
¬r x' x
theorem Ordinal.typein_le_typein' (o : Ordinal.{u_3}) {x : (Quotient.out o)} {x' : (Quotient.out o)} :
Ordinal.typein (fun (x x_1 : (Quotient.out o)) => x < x_1) x Ordinal.typein (fun (x x_1 : (Quotient.out o)) => x < x_1) x' x x'
@[simp]
theorem Ordinal.enum_le_enum {α : Type u} (r : ααProp) [] {o : Ordinal.{u}} {o' : Ordinal.{u}} (ho : ) (ho' : o' < ) :
¬r (Ordinal.enum r o' ho') (Ordinal.enum r o ho) o o'
@[simp]
theorem Ordinal.enum_le_enum' (a : Ordinal.{u_3}) {o : Ordinal.{u_3}} {o' : Ordinal.{u_3}} (ho : o < Ordinal.type fun (x x_1 : (Quotient.out a)) => x < x_1) (ho' : o' < Ordinal.type fun (x x_1 : (Quotient.out a)) => x < x_1) :
Ordinal.enum (fun (x x_1 : (Quotient.out a)) => x < x_1) o ho Ordinal.enum (fun (x x_1 : (Quotient.out a)) => x < x_1) o' ho' o o'
theorem Ordinal.enum_zero_le {α : Type u} {r : ααProp} [] (h0 : ) (a : α) :
¬r a (Ordinal.enum r 0 h0)
theorem Ordinal.enum_zero_le' {o : Ordinal.{u_3}} (h0 : 0 < o) (a : (Quotient.out o)) :
Ordinal.enum (fun (x x_1 : (Quotient.out o)) => x < x_1) 0 a
theorem Ordinal.le_enum_succ {o : Ordinal.{u_3}} (a : (Quotient.out (Order.succ o))) :
a Ordinal.enum (fun (x x_1 : (Quotient.out (Order.succ o))) => x < x_1) o
@[simp]
theorem Ordinal.enum_inj {α : Type u} {r : ααProp} [] {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (h₁ : o₁ < ) (h₂ : o₂ < ) :
Ordinal.enum r o₁ h₁ = Ordinal.enum r o₂ h₂ o₁ = o₂
@[simp]
theorem Ordinal.enumIso_apply {α : Type u} (r : ααProp) [] (x : fun (x : Ordinal.{u}) => ) :
x = Ordinal.enum r x
@[simp]
theorem Ordinal.enumIso_symm_apply_coe {α : Type u} (r : ααProp) [] (x : α) :
(.symm x) =
def Ordinal.enumIso {α : Type u} (r : ααProp) [] :
(Subrel (fun (x x_1 : Ordinal.{u}) => x < x_1) fun (x : Ordinal.{u}) => ) ≃r r

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Ordinal.enumIsoOut_symm_apply_coe (o : Ordinal.{u_3}) (x : (Quotient.out o)) :
((RelIso.symm o.enumIsoOut) x) = Ordinal.typein (fun (x x_1 : (Quotient.out o)) => x < x_1) x
@[simp]
theorem Ordinal.enumIsoOut_apply (o : Ordinal.{u_3}) (x : (Set.Iio o)) :
o.enumIsoOut x = Ordinal.enum (fun (x x_1 : (Quotient.out o)) => x < x_1) x
noncomputable def Ordinal.enumIsoOut (o : Ordinal.{u_3}) :
(Set.Iio o) ≃o (Quotient.out o)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
Instances For
theorem Ordinal.enum_zero_eq_bot {o : Ordinal.{u_3}} (ho : 0 < o) :
Ordinal.enum (fun (x x_1 : (Quotient.out o)) => x < x_1) 0 =

Universal 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
Instances For
@[simp]
def Ordinal.lift.principalSeg :
(fun (x x_1 : Ordinal.{u}) => x < x_1) ≺i fun (x x_1 : Ordinal.{max (u + 1) v} ) => x < x_1

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

Equations
Instances For
@[simp]

Representing a cardinal with an ordinal #

The ordinal corresponding to a cardinal c is the least ordinal whose cardinal is c. For the order-embedding version, see ord.order_embedding.

Equations
• c.ord = let F := fun (α : Type u) => ⨅ (r : { r : ααProp // }), ;
Instances For
theorem Cardinal.ord_eq_Inf (α : Type u) :
(Cardinal.mk α).ord = ⨅ (r : { r : ααProp // }),
theorem Cardinal.ord_eq (α : Type u_3) :
∃ (r : ααProp) (wo : ), (Cardinal.mk α).ord =
theorem Cardinal.ord_le_type {α : Type u} (r : ααProp) [h : ] :
(Cardinal.mk α).ord
theorem Cardinal.ord_le {c : Cardinal.{u_3}} {o : Ordinal.{u_3}} :
c.ord o c o.card
theorem Cardinal.lt_ord {c : Cardinal.{u_3}} {o : Ordinal.{u_3}} :
o < c.ord o.card < c
@[simp]
theorem Cardinal.card_ord (c : Cardinal.{u_3}) :
c.ord.card = c

Galois coinsertion between Cardinal.ord and Ordinal.card.

Equations
Instances For
theorem Cardinal.ord_card_le (o : Ordinal.{u_3}) :
o.card.ord o
theorem Cardinal.card_le_of_le_ord {o : Ordinal.{u_3}} {c : Cardinal.{u_3}} (ho : o c.ord) :
o.card c

A variation on Cardinal.lt_ord using ≤: If o is no greater than the initial ordinal of cardinality c, then its cardinal is no greater than c.

The converse, however, is false (for instance, o = ω+1 and c = ℵ₀).

@[simp]
theorem Cardinal.ord_le_ord {c₁ : Cardinal.{u_3}} {c₂ : Cardinal.{u_3}} :
c₁.ord c₂.ord c₁ c₂
@[simp]
theorem Cardinal.ord_lt_ord {c₁ : Cardinal.{u_3}} {c₂ : Cardinal.{u_3}} :
c₁.ord < c₂.ord c₁ < c₂
@[simp]
@[simp]
theorem Cardinal.ord_nat (n : ) :
(↑n).ord = n
@[simp]
@[simp]
theorem Cardinal.ord_ofNat (n : ) [n.AtLeastTwo] :
(OfNat.ofNat n).ord =
@[simp]
theorem Cardinal.card_typein_lt {α : Type u} (r : ααProp) [] (x : α) (h : (Cardinal.mk α).ord = ) :
(Ordinal.typein r x).card <
theorem Cardinal.card_typein_out_lt (c : Cardinal.{u_3}) (x : (Quotient.out c.ord)) :
(Ordinal.typein (fun (x x_1 : (Quotient.out c.ord)) => x < x_1) x).card < c

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

The cardinal univ is the cardinality of ordinal univ, or equivalently the cardinal of Ordinal.{u}, or Cardinal.{u}, as an element of Cardinal.{v} (when u < v).

Equations
Instances For
@[simp]
@[simp]
theorem Cardinal.lt_univ {c : Cardinal.{u + 1} } :
∃ (c' : Cardinal.{u}), c =
theorem Cardinal.lt_univ' :
∃ (c' : Cardinal.{u}), c =
@[simp]
@[simp]
theorem Ordinal.nat_le_card {o : Ordinal.{u_3}} {n : } :
n o.card n o
@[simp]
theorem Ordinal.one_le_card {o : Ordinal.{u_3}} :
1 o.card 1 o
@[simp]
theorem Ordinal.ofNat_le_card {o : Ordinal.{u_3}} {n : } [n.AtLeastTwo] :
o.card o
@[simp]
theorem Ordinal.nat_lt_card {o : Ordinal.{u_3}} {n : } :
n < o.card n < o
@[simp]
theorem Ordinal.zero_lt_card {o : Ordinal.{u_3}} :
0 < o.card 0 < o
@[simp]
theorem Ordinal.one_lt_card {o : Ordinal.{u_3}} :
1 < o.card 1 < o
@[simp]
theorem Ordinal.ofNat_lt_card {o : Ordinal.{u_3}} {n : } [n.AtLeastTwo] :
< o.card < o
@[simp]
theorem Ordinal.card_lt_nat {o : Ordinal.{u_3}} {n : } :
o.card < n o < n
@[simp]
theorem Ordinal.card_lt_ofNat {o : Ordinal.{u_3}} {n : } [n.AtLeastTwo] :
o.card < o <
@[simp]
theorem Ordinal.card_le_nat {o : Ordinal.{u_3}} {n : } :
o.card n o n
@[simp]
theorem Ordinal.card_le_one {o : Ordinal.{u_3}} :
o.card 1 o 1
@[simp]
theorem Ordinal.card_le_ofNat {o : Ordinal.{u_3}} {n : } [n.AtLeastTwo] :
o.card o
@[simp]
theorem Ordinal.card_eq_nat {o : Ordinal.{u_3}} {n : } :
o.card = n o = n
@[simp]
theorem Ordinal.card_eq_zero {o : Ordinal.{u_3}} :
o.card = 0 o = 0
@[simp]
theorem Ordinal.card_eq_one {o : Ordinal.{u_3}} :
o.card = 1 o = 1
@[simp]
theorem Ordinal.card_eq_ofNat {o : Ordinal.{u_3}} {n : } [n.AtLeastTwo] :
o.card = o =
@[simp]
theorem Ordinal.type_fintype {α : Type u} (r : ααProp) [] [] :
= (Fintype.card α)
theorem Ordinal.type_fin (n : ) :
(Ordinal.type fun (x x_1 : Fin n) => x < x_1) = n

Sorted lists #

theorem List.Sorted.lt_ord_of_lt {α : Type u} [] [IsWellOrder α fun (x x_1 : α) => x < x_1] {l : List α} {m : List α} {o : Ordinal.{u}} (hl : List.Sorted (fun (x x_1 : α) => x > x_1) l) (hm : List.Sorted (fun (x x_1 : α) => x > x_1) m) (hmltl : m < l) (hlt : il, Ordinal.typein (fun (x x_1 : α) => x < x_1) i < o) (i : α) :
i mOrdinal.typein (fun (x x_1 : α) => x < x_1) i < o