Documentation

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

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 OrdinalArithmetic.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.{u})

def embeddingToCardinal {σ : Type u} :

σ ↪ Cardinal.{u}

An embedding of any type to the set of cardinals.

Equations

embeddingToCardinal = Classical.choice (_ : Nonempty (σ ↪ Cardinal.{u}))

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

WellOrderingRel = ↑embeddingToCardinal ⁻¹'o fun x x_1 => x < x_1

Instances For

instance WellOrderingRel.isWellOrder {σ : Type u} :

IsWellOrder σ WellOrderingRel

Equations

@WellOrderingRel.isWellOrder = @WellOrderingRel.isWellOrder.proof_1

instance IsWellOrder.subtype_nonempty {σ : Type u} :

Nonempty { r // IsWellOrder σ r }

Equations

@IsWellOrder.subtype_nonempty = @IsWellOrder.subtype_nonempty.proof_1

Definition of ordinals #

structure WellOrder :

Type (u + 1)

α : Type u
The underlying type of the order.
r : s.α → s.α → Prop
The underlying relation of the order.
wo : IsWellOrder s.α s.r
The proposition that r is a well-ordering for α.

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

Instances For

instance WellOrder.inhabited :

Inhabited WellOrder

Equations

WellOrder.inhabited = { default := { α := PEmpty.{u_3 + 1} , r := EmptyRelation, wo := WellOrder.inhabited.proof_1 } }

@[simp]

theorem WellOrder.eta (o : WellOrder) :

{ α := o.α, r := o.r, wo := (_ : IsWellOrder o.α o.r) } = o

instance Ordinal.isEquivalent :

Setoid WellOrder

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.

Type (u + 1)

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

Equations

Ordinal.{u} = Quotient Ordinal.isEquivalent

Instances For

instance hasWellFoundedOut (o : Ordinal.{u_3}) :

WellFoundedRelation (Quotient.out o).α

Equations

hasWellFoundedOut o = { rel := (Quotient.out o).r, wf := (_ : WellFounded (Quotient.out o).r) }

instance linearOrderOut (o : Ordinal.{u_3}) :

LinearOrder (Quotient.out o).α

Equations

linearOrderOut o = IsWellOrder.linearOrder (Quotient.out o).r

instance isWellOrder_out_lt (o : Ordinal.{u_3}) :

IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1

Equations

isWellOrder_out_lt = isWellOrder_out_lt.proof_1

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

The order type of a well order is an ordinal.

Equations

Ordinal.type r = Quotient.mk Ordinal.isEquivalent { α := α, r := r, wo := wo }

Instances For

instance Ordinal.zero :

Zero Ordinal.{u_3}

Equations

Ordinal.zero = { zero := Ordinal.type EmptyRelation }

instance Ordinal.inhabited :

Inhabited Ordinal.{u_3}

Equations

Ordinal.inhabited = { default := 0 }

instance Ordinal.one :

One Ordinal.{u_3}

Equations

Ordinal.one = { one := Ordinal.type EmptyRelation }

def Ordinal.typein {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] (a : α) :

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

Equations

Ordinal.typein r a = Ordinal.type (Subrel r {b | r b a})

Instances For

@[simp]

theorem Ordinal.type_def' (w : WellOrder) :

Quotient.mk Ordinal.isEquivalent w = Ordinal.type w.r

@[simp]

theorem Ordinal.type_def {α : Type u_3} (r : α → α → Prop) [wo : IsWellOrder α r] :

Quotient.mk Ordinal.isEquivalent { α := α, r := r, wo := wo } = Ordinal.type r

@[simp]

theorem Ordinal.type_out (o : Ordinal.{u_3}) :

Ordinal.type (Quotient.out o).r = o

theorem Ordinal.type_eq {α : Type u_3} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] :

Ordinal.type r = Ordinal.type s ↔ Nonempty (r ≃r s)

theorem RelIso.ordinal_type_eq {α : Type u_3} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : r ≃r s) :

Ordinal.type r = Ordinal.type s

@[simp]

theorem Ordinal.type_lt (o : Ordinal.{u_3}) :

(Ordinal.type fun x x_1 => x < x_1) = o

theorem Ordinal.type_eq_zero_of_empty {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] [IsEmpty α] :

Ordinal.type r = 0

@[simp]

theorem Ordinal.type_eq_zero_iff_isEmpty {α : Type u_3} {r : α → α → Prop} [IsWellOrder α r] :

Ordinal.type r = 0 ↔ IsEmpty α

theorem Ordinal.type_ne_zero_iff_nonempty {α : Type u_3} {r : α → α → Prop} [IsWellOrder α r] :

Ordinal.type r ≠ 0 ↔ Nonempty α

theorem Ordinal.type_ne_zero_of_nonempty {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] [h : Nonempty α] :

Ordinal.type r ≠ 0

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_3} (r : α → α → Prop) [IsWellOrder α r] [Unique α] :

Ordinal.type r = 1

@[simp]

theorem Ordinal.type_eq_one_iff_unique {α : Type u_3} {r : α → α → Prop} [IsWellOrder α r] :

Ordinal.type r = 1 ↔ Nonempty (Unique α)

theorem Ordinal.type_pUnit :

Ordinal.type EmptyRelation = 1

theorem Ordinal.type_unit :

Ordinal.type EmptyRelation = 1

@[simp]

theorem Ordinal.out_empty_iff_eq_zero {o : Ordinal.{u_3}} :

IsEmpty (Quotient.out o).α ↔ o = 0

theorem Ordinal.eq_zero_of_out_empty (o : Ordinal.{u_3}) [h : IsEmpty (Quotient.out o).α] :

o = 0

instance Ordinal.isEmpty_out_zero :

IsEmpty (Quotient.out 0).α

Equations

Ordinal.isEmpty_out_zero = Ordinal.isEmpty_out_zero.proof_1

@[simp]

theorem Ordinal.out_nonempty_iff_ne_zero {o : Ordinal.{u_3}} :

Nonempty (Quotient.out o).α ↔ o ≠ 0

theorem Ordinal.ne_zero_of_out_nonempty (o : Ordinal.{u_3}) [h : Nonempty (Quotient.out o).α] :

o ≠ 0

theorem Ordinal.one_ne_zero :

1 ≠ 0

instance Ordinal.nontrivial :

Nontrivial Ordinal.{u}

Equations

Ordinal.nontrivial = Ordinal.nontrivial.proof_1

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

Ordinal.type (↑f ⁻¹'o r) = Ordinal.type r

@[simp]

theorem Ordinal.type_preimage_aux {α : Type u} {β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) :

(Ordinal.type fun x y => r (↑f x) (↑f y)) = Ordinal.type r

theorem Ordinal.inductionOn {C : Ordinal.{u_3} → Prop} (o : Ordinal.{u_3}) (H : (α : Type u_3) → (r : α → α → Prop) → [inst : IsWellOrder α r] → C (Ordinal.type r)) :

C o

The order on ordinals #

instance Ordinal.partialOrder :

PartialOrder Ordinal.{u_3}

Equations

Ordinal.partialOrder = PartialOrder.mk Ordinal.partialOrder.proof_6

theorem Ordinal.type_le_iff {α : Type u_3} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] :

Ordinal.type r ≤ Ordinal.type s ↔ Nonempty (r ≼i s)

theorem Ordinal.type_le_iff' {α : Type u_3} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] :

Ordinal.type r ≤ Ordinal.type s ↔ Nonempty (r ↪r s)

theorem InitialSeg.ordinal_type_le {α : Type u_3} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : r ≼i s) :

Ordinal.type r ≤ Ordinal.type s

theorem RelEmbedding.ordinal_type_le {α : Type u_3} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : r ↪r s) :

Ordinal.type r ≤ Ordinal.type s

@[simp]

theorem Ordinal.type_lt_iff {α : Type u_3} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] :

Ordinal.type r < Ordinal.type s ↔ Nonempty (r ≺i s)

theorem PrincipalSeg.ordinal_type_lt {α : Type u_3} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : r ≺i s) :

Ordinal.type r < Ordinal.type s

theorem Ordinal.zero_le (o : Ordinal.{u_3}) :

0 ≤ o

instance Ordinal.orderBot :

OrderBot Ordinal.{u_3}

Equations

Ordinal.orderBot = OrderBot.mk Ordinal.zero_le

@[simp]

theorem Ordinal.bot_eq_zero :

@[simp]

theorem Ordinal.le_zero {o : Ordinal.{u_3}} :

o ≤ 0 ↔ o = 0

theorem Ordinal.pos_iff_ne_zero {o : Ordinal.{u_3}} :

0 < o ↔ o ≠ 0

theorem Ordinal.not_lt_zero (o : Ordinal.{u_3}) :

¬o < 0

theorem Ordinal.eq_zero_or_pos (a : Ordinal.{u_3}) :

a = 0 ∨ 0 < a

instance Ordinal.zeroLEOneClass :

ZeroLEOneClass Ordinal.{u_3}

Equations

Ordinal.zeroLEOneClass = Ordinal.zeroLEOneClass.proof_1

instance Ordinal.NeZero.one :

Equations

Ordinal.NeZero.one = Ordinal.NeZero.one.proof_1

def Ordinal.initialSegOut {α : Ordinal.{u_3}} {β : Ordinal.{u_3}} (h : α ≤ β) :

(fun x x_1 => x < x_1) ≼i fun x x_1 => 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 => x < x_1) ≺i fun x x_1 => 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_3} (r : α → α → Prop) [IsWellOrder α r] (a : α) :

Ordinal.typein r a < Ordinal.type r

theorem Ordinal.typein_lt_self {o : Ordinal.{u_3}} (i : (Quotient.out o).α) :

Ordinal.typein (fun x x_1 => x < x_1) i < o

@[simp]

theorem Ordinal.typein_top {α : Type u_3} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≺i s) :

Ordinal.typein s f.top = Ordinal.type r

@[simp]

theorem Ordinal.typein_apply {α : Type u_3} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≼i s) (a : α) :

Ordinal.typein s (↑f a) = Ordinal.typein r a

@[simp]

theorem Ordinal.typein_lt_typein {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] {a : α} {b : α} :

Ordinal.typein r a < Ordinal.typein r b ↔ r a b

theorem Ordinal.typein_surj {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] {o : Ordinal.{u_3}} (h : o < Ordinal.type r) :

∃ a, Ordinal.typein r a = o

theorem Ordinal.typein_injective {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] :

Function.Injective (Ordinal.typein r)

@[simp]

theorem Ordinal.typein_inj {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] {a : α} {b : α} :

Ordinal.typein r a = Ordinal.typein r b ↔ a = b

def Ordinal.typein.principalSeg {α : Type u} (r : α → α → Prop) [IsWellOrder α r] :

r ≺i fun x x_1 => x < x_1

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

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem Ordinal.typein.principalSeg_coe {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] :

↑(Ordinal.typein.principalSeg r).toRelEmbedding = Ordinal.typein r

Enumerating elements in a well-order with ordinals. #

def Ordinal.enum {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] (o : Ordinal.{u_3}) (h : 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 h = ↑(PrincipalSeg.subrelIso (Ordinal.typein.principalSeg r)) { val := o, property := h }

Instances For

@[simp]

theorem Ordinal.typein_enum {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] {o : Ordinal.{u_3}} (h : o < Ordinal.type r) :

Ordinal.typein r (Ordinal.enum r o h) = o

theorem Ordinal.enum_type {α : Type u_3} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : s ≺i r) {h : Ordinal.type s < Ordinal.type r} :

Ordinal.enum r (Ordinal.type s) h = f.top

@[simp]

theorem Ordinal.enum_typein {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] (a : α) :

Ordinal.enum r (Ordinal.typein r a) (_ : Ordinal.typein r a < Ordinal.type r) = a

theorem Ordinal.enum_lt_enum {α : Type u_3} {r : α → α → Prop} [IsWellOrder α r] {o₁ : Ordinal.{u_3}} {o₂ : Ordinal.{u_3}} (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.relIso_enum' {α : Type u} {β : Type u} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) (o : Ordinal.{u}) (hr : o < Ordinal.type r) (hs : o < Ordinal.type s) :

↑f (Ordinal.enum r o hr) = Ordinal.enum s o hs

theorem Ordinal.relIso_enum {α : Type u} {β : Type u} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) (o : Ordinal.{u}) (hr : o < Ordinal.type r) :

↑f (Ordinal.enum r o hr) = Ordinal.enum s o (_ : o < Ordinal.type s)

theorem Ordinal.lt_wf :

WellFounded fun x x_1 => x < x_1

instance Ordinal.wellFoundedRelation :

WellFoundedRelation Ordinal.{u_3}

Equations

Ordinal.wellFoundedRelation = { rel := fun x x_1 => x < x_1, wf := Ordinal.lt_wf }

theorem Ordinal.induction {p : Ordinal.{u} → Prop} (i : Ordinal.{u}) (h : (j : Ordinal.{u}) → ((k : 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 i IH.

Cardinality of ordinals #

def Ordinal.card :

Ordinal.{u_3} → Cardinal.{u_3}

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 WellOrder.α Ordinal.card.proof_1

Instances For

@[simp]

theorem Ordinal.card_type {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] :

Ordinal.card (Ordinal.type r) = Cardinal.mk α

@[simp]

theorem Ordinal.card_typein {α : Type u_3} {r : α → α → Prop} [IsWellOrder α r] (x : α) :

Cardinal.mk { y // r y x } = Ordinal.card (Ordinal.typein r x)

theorem Ordinal.card_le_card {o₁ : Ordinal.{u_3}} {o₂ : Ordinal.{u_3}} :

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

@[simp]

theorem Ordinal.card_zero :

Ordinal.card 0 = 0

@[simp]

theorem Ordinal.card_eq_zero {o : Ordinal.{u_3}} :

Ordinal.card o = 0 ↔ o = 0

@[simp]

theorem Ordinal.card_one :

Ordinal.card 1 = 1

Lifting ordinals to a higher universe #

def Ordinal.lift (o : Ordinal.{v}) :

Ordinal.{max v u}

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

Ordinal.lift.{u, v} o = Quotient.liftOn o (fun w => Ordinal.type (ULift.down ⁻¹'o w.r)) Ordinal.lift.proof_2

Instances For

theorem Ordinal.type_uLift {α : Type u} (r : α → α → Prop) [IsWellOrder α r] :

Ordinal.type (ULift.down ⁻¹'o r) = Ordinal.lift.{v, u} (Ordinal.type r)

@[simp]

theorem Ordinal.type_uLift_aux {α : Type u} (r : α → α → Prop) [IsWellOrder α r] :

(Ordinal.type fun x y => r x.down y.down) = Ordinal.lift.{v, u} (Ordinal.type r)

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

Ordinal.lift.{v, u} (Ordinal.type r) = Ordinal.lift.{u, v} (Ordinal.type s)

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

Ordinal.lift.{u, v} (Ordinal.type (↑f ⁻¹'o r)) = Ordinal.lift.{v, u} (Ordinal.type r)

@[simp]

theorem Ordinal.type_lift_preimage_aux {α : Type u} {β : Type v} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) :

Ordinal.lift.{u, v} (Ordinal.type fun x y => r (↑f x) (↑f y)) = Ordinal.lift.{v, u} (Ordinal.type r)

theorem Ordinal.lift_umax :

Ordinal.lift.{max u v, u} = Ordinal.lift.{v, u}

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

theorem Ordinal.lift_umax' :

Ordinal.lift.{max v u, u} = Ordinal.lift.{v, u}

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

theorem Ordinal.lift_id' (a : Ordinal.{max u_3 u_4} ) :

Ordinal.lift.{u_3, max u_3 u_4} a = a

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

@[simp]

theorem Ordinal.lift_id (a : Ordinal.{u}) :

Ordinal.lift.{u, u} a = a

An ordinal lifted to the same universe equals itself.

@[simp]

theorem Ordinal.lift_uzero (a : Ordinal.{u}) :

Ordinal.lift.{0, u} a = a

An ordinal lifted to the zero universe equals itself.

@[simp]

theorem Ordinal.lift_lift (a : Ordinal.{u_3}) :

Ordinal.lift.{w, max v u_3} (Ordinal.lift.{v, u_3} a) = Ordinal.lift.{max v w, u_3} a

theorem Ordinal.lift_type_le {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] :

Ordinal.lift.{max v w, u} (Ordinal.type r) ≤ Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (r ≼i s)

theorem Ordinal.lift_type_eq {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] :

Ordinal.lift.{max v w, u} (Ordinal.type r) = Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (r ≃r s)

theorem Ordinal.lift_type_lt {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] :

Ordinal.lift.{max v w, u} (Ordinal.type r) < Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (r ≺i s)

@[simp]

theorem Ordinal.lift_le {a : Ordinal.{v}} {b : Ordinal.{v}} :

Ordinal.lift.{u, v} a ≤ Ordinal.lift.{u, v} b ↔ a ≤ b

@[simp]

theorem Ordinal.lift_inj {a : Ordinal.{v}} {b : Ordinal.{v}} :

Ordinal.lift.{u, v} a = Ordinal.lift.{u, v} b ↔ a = b

@[simp]

theorem Ordinal.lift_lt {a : Ordinal.{v}} {b : Ordinal.{v}} :

Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} b ↔ a < b

@[simp]

theorem Ordinal.lift_zero :

Ordinal.lift.{u_4, u_3} 0 = 0

@[simp]

theorem Ordinal.lift_one :

Ordinal.lift.{u_4, u_3} 1 = 1

@[simp]

theorem Ordinal.lift_card (a : Ordinal.{v}) :

Cardinal.lift.{u, v} (Ordinal.card a) = Ordinal.card (Ordinal.lift.{u, v} a)

theorem Ordinal.lift_down' {a : Cardinal.{u}} {b : Ordinal.{max u v} } (h : Ordinal.card b ≤ Cardinal.lift.{v, u} a) :

∃ a', Ordinal.lift.{v, u} a' = b

theorem Ordinal.lift_down {a : Ordinal.{u}} {b : Ordinal.{max u v} } (h : b ≤ Ordinal.lift.{v, u} a) :

∃ a', Ordinal.lift.{v, u} a' = b

theorem Ordinal.le_lift_iff {a : Ordinal.{u}} {b : Ordinal.{max u v} } :

b ≤ Ordinal.lift.{v, u} a ↔ ∃ a', Ordinal.lift.{v, u} a' = b ∧ a' ≤ a

theorem Ordinal.lt_lift_iff {a : Ordinal.{u}} {b : Ordinal.{max u v} } :

b < Ordinal.lift.{v, u} a ↔ ∃ a', Ordinal.lift.{v, u} a' = b ∧ a' < a

def Ordinal.lift.initialSeg :

(fun x x_1 => x < x_1) ≼i fun x x_1 => 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

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem Ordinal.lift.initialSeg_coe :

↑Ordinal.lift.initialSeg = Ordinal.lift.{v, u}

The first infinite ordinal `omega` #

def Ordinal.omega :

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

Equations

Ordinal.omega = Ordinal.lift.{u, 0} (Ordinal.type fun x x_1 => x < x_1)

Instances For

def Ordinal.termω :

Lean.ParserDescr

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

Equations

Ordinal.termω = Lean.ParserDescr.node `Ordinal.termω 1024 (Lean.ParserDescr.symbol "ω")

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]

theorem Ordinal.card_omega :

Ordinal.card Ordinal.omega = Cardinal.aleph0

@[simp]

theorem Ordinal.lift_omega :

Ordinal.lift.{u_3, u_4} Ordinal.omega = 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 OrdinalArithmetic.lean.

instance Ordinal.add :

Add Ordinal.{u}

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.

instance Ordinal.addMonoidWithOne :

AddMonoidWithOne Ordinal.{u}

Equations

Ordinal.addMonoidWithOne = AddMonoidWithOne.mk

@[simp]

theorem Ordinal.card_add (o₁ : Ordinal.{u_3}) (o₂ : Ordinal.{u_3}) :

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

@[simp]

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

Ordinal.type (Sum.Lex r s) = Ordinal.type r + Ordinal.type s

@[simp]

theorem Ordinal.card_nat (n : ℕ) :

Ordinal.card ↑n = ↑n

instance Ordinal.add_covariantClass_le :

CovariantClass Ordinal.{u} Ordinal.{u} (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

Ordinal.add_covariantClass_le = Ordinal.add_covariantClass_le.proof_1

instance Ordinal.add_swap_covariantClass_le :

CovariantClass Ordinal.{u} Ordinal.{u} (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

Ordinal.add_swap_covariantClass_le = Ordinal.add_swap_covariantClass_le.proof_1

theorem Ordinal.le_add_right (a : Ordinal.{u_3}) (b : Ordinal.{u_3}) :

a ≤ a + b

theorem Ordinal.le_add_left (a : Ordinal.{u_3}) (b : Ordinal.{u_3}) :

a ≤ b + a

instance Ordinal.linearOrder :

LinearOrder Ordinal.{u_3}

Equations

One or more equations did not get rendered due to their size.

instance Ordinal.wellFoundedLT :

WellFoundedLT Ordinal.{u_3}

Equations

Ordinal.wellFoundedLT = Ordinal.wellFoundedLT.proof_1

instance Ordinal.isWellOrder :

IsWellOrder Ordinal.{u_3} fun x x_1 => x < x_1

Equations

Ordinal.isWellOrder = Ordinal.isWellOrder.proof_1

instance Ordinal.instConditionallyCompleteLinearOrderBotOrdinal :

ConditionallyCompleteLinearOrderBot Ordinal.{u_3}

Equations

Ordinal.instConditionallyCompleteLinearOrderBotOrdinal = IsWellOrder.conditionallyCompleteLinearOrderBot Ordinal.{u_3}

@[simp]

theorem Ordinal.max_zero_left (a : Ordinal.{u_3}) :

max 0 a = a

@[simp]

theorem Ordinal.max_zero_right (a : Ordinal.{u_3}) :

max a 0 = a

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

instance Ordinal.noMaxOrder :

NoMaxOrder Ordinal.{u_3}

Equations

Ordinal.noMaxOrder = Ordinal.noMaxOrder.proof_1

instance Ordinal.succOrder :

SuccOrder Ordinal.{u}

Equations

Ordinal.succOrder = SuccOrder.ofSuccLeIff (fun o => o + 1) (_ : ∀ {a b : Ordinal.{u}}, a + 1 ≤ b ↔ a < b)

@[simp]

theorem Ordinal.add_one_eq_succ (o : Ordinal.{u_3}) :

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₁ : Ordinal.{u_3}) (o₂ : Ordinal.{u_3}) :

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

theorem Ordinal.one_le_iff_pos {o : Ordinal.{u_3}} :

1 ≤ o ↔ 0 < o

theorem Ordinal.one_le_iff_ne_zero {o : Ordinal.{u_3}} :

1 ≤ o ↔ o ≠ 0

theorem Ordinal.succ_pos (o : Ordinal.{u_3}) :

0 < Order.succ o

theorem Ordinal.succ_ne_zero (o : Ordinal.{u_3}) :

Order.succ o ≠ 0

theorem Ordinal.lt_one_iff_zero {a : Ordinal.{u_3}} :

a < 1 ↔ a = 0

theorem Ordinal.le_one_iff {a : Ordinal.{u_3}} :

a ≤ 1 ↔ a = 0 ∨ a = 1

@[simp]

theorem Ordinal.card_succ (o : Ordinal.{u_3}) :

Ordinal.card (Order.succ o) = Ordinal.card o + 1

theorem Ordinal.nat_cast_succ (n : ℕ) :

↑(Nat.succ n) = Order.succ ↑n

instance Ordinal.uniqueIioOne :

Unique ↑(Set.Iio 1)

Equations

Ordinal.uniqueIioOne = { toInhabited := { default := { val := 0, property := Ordinal.uniqueIioOne.proof_1 } }, uniq := Ordinal.uniqueIioOne.proof_2 }

instance Ordinal.uniqueOutOne :

Unique (Quotient.out 1).α

Equations

Ordinal.uniqueOutOne = { toInhabited := { default := Ordinal.enum (fun x x_1 => x < x_1) 0 Ordinal.uniqueOutOne.proof_2 }, uniq := Ordinal.uniqueOutOne.proof_3 }

theorem Ordinal.one_out_eq (x : (Quotient.out 1).α) :

x = Ordinal.enum (fun x x_1 => x < x_1) 0 (_ : 0 < Ordinal.type fun x x_1 => x < x_1)

Extra properties of typein and enum #

@[simp]

theorem Ordinal.typein_one_out (x : (Quotient.out 1).α) :

Ordinal.typein (fun x x_1 => x < x_1) x = 0

@[simp]

theorem Ordinal.typein_le_typein {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] {x : α} {x' : α} :

Ordinal.typein r x ≤ Ordinal.typein r 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 => x < x_1) x ≤ Ordinal.typein (fun x x_1 => x < x_1) x' ↔ x ≤ x'

@[simp]

theorem Ordinal.enum_le_enum {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] {o : Ordinal.{u_3}} {o' : Ordinal.{u_3}} (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.{u_3}) {o : Ordinal.{u_3}} {o' : Ordinal.{u_3}} (ho : o < Ordinal.type fun x x_1 => x < x_1) (ho' : o' < Ordinal.type fun x x_1 => x < x_1) :

Ordinal.enum (fun x x_1 => x < x_1) o ho ≤ Ordinal.enum (fun x x_1 => x < x_1) o' ho' ↔ o ≤ o'

theorem Ordinal.enum_zero_le {α : Type u_3} {r : α → α → Prop} [IsWellOrder α r] (h0 : 0 < Ordinal.type r) (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 => x < x_1) 0 (_ : 0 < Ordinal.type fun x x_1 => x < x_1) ≤ a

theorem Ordinal.le_enum_succ {o : Ordinal.{u_3}} (a : (Quotient.out (Order.succ o)).α) :

a ≤ Ordinal.enum (fun x x_1 => x < x_1) o (_ : o < Ordinal.type fun x x_1 => x < x_1)

@[simp]

theorem Ordinal.enum_inj {α : Type u_3} {r : α → α → Prop} [IsWellOrder α r] {o₁ : Ordinal.{u_3}} {o₂ : Ordinal.{u_3}} (h₁ : o₁ < Ordinal.type r) (h₂ : o₂ < Ordinal.type r) :

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

@[simp]

theorem Ordinal.enumIso_symm_apply_coe {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] (x : α) :

↑(↑(RelIso.symm (Ordinal.enumIso r)) x) = Ordinal.typein r x

@[simp]

theorem Ordinal.enumIso_apply {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] (x : ↑fun x => x < Ordinal.type r) :

↑(Ordinal.enumIso r) x = Ordinal.enum r ↑x (_ : ↑x ∈ fun x => x < Ordinal.type r)

def Ordinal.enumIso {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] :

(Subrel (fun x x_1 => x < x_1) fun x => x < Ordinal.type r) ≃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 (Ordinal.enumIsoOut o)) x) = Ordinal.typein (fun x x_1 => x < x_1) x

@[simp]

theorem Ordinal.enumIsoOut_apply (o : Ordinal.{u_3}) (x : ↑(Set.Iio o)) :

↑(Ordinal.enumIsoOut o) x = Ordinal.enum (fun x x_1 => x < x_1) ↑x (_ : ↑x < Ordinal.type fun x x_1 => x < x_1)

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

def Ordinal.outOrderBotOfPos {o : Ordinal.{u_3}} (ho : 0 < o) :

OrderBot (Quotient.out o).α

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

Equations

Ordinal.outOrderBotOfPos ho = OrderBot.mk (_ : ∀ (a : (Quotient.out o).α), Ordinal.enum (fun x x_1 => x < x_1) 0 (_ : 0 < Ordinal.type fun x x_1 => x < x_1) ≤ a)

Instances For

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

Ordinal.enum (fun x x_1 => x < x_1) 0 (_ : 0 < Ordinal.type fun x x_1 => x < x_1) = ⊥

Universal ordinal #

def Ordinal.univ :

Ordinal.{max (u + 1) v}

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.lift.{v, u + 1} (Ordinal.type fun x x_1 => x < x_1)

Instances For

theorem Ordinal.univ_id :

Ordinal.univ = Ordinal.type fun x x_1 => x < x_1

@[simp]

theorem Ordinal.lift_univ :

Ordinal.lift.{w, max (u + 1) v} Ordinal.univ = Ordinal.univ

theorem Ordinal.univ_umax :

Ordinal.univ = Ordinal.univ

def Ordinal.lift.principalSeg :

(fun x x_1 => x < x_1) ≺i fun x x_1 => 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

Ordinal.lift.principalSeg = { toRelEmbedding := Ordinal.lift.initialSeg.toRelEmbedding, top := Ordinal.univ, down' := Ordinal.lift.principalSeg.proof_1 }

Instances For

@[simp]

theorem Ordinal.lift.principalSeg_coe :

↑Ordinal.lift.principalSeg.toRelEmbedding = Ordinal.lift.{max (u + 1) v, u}

@[simp]

theorem Ordinal.lift.principalSeg_top :

Ordinal.lift.principalSeg.top = Ordinal.univ

theorem Ordinal.lift.principalSeg_top' :

Ordinal.lift.principalSeg.top = Ordinal.type fun x x_1 => x < x_1

Representing a cardinal with an ordinal #

@[simp]

theorem Cardinal.mk_ordinal_out (o : Ordinal.{u_3}) :

Cardinal.mk (Quotient.out o).α = Ordinal.card o

def Cardinal.ord (c : Cardinal.{u}) :

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

Cardinal.ord c = let F := fun α => ⨅ (r : { r // IsWellOrder α r }), Ordinal.type ↑r; Quot.liftOn c F Cardinal.ord.proof_2

Instances For

theorem Cardinal.ord_eq_Inf (α : Type u) :

Cardinal.ord (Cardinal.mk α) = ⨅ (r : { r // IsWellOrder α r }), Ordinal.type ↑r

theorem Cardinal.ord_eq (α : Type u_3) :

∃ r wo, Cardinal.ord (Cardinal.mk α) = Ordinal.type r

theorem Cardinal.ord_le_type {α : Type u_3} (r : α → α → Prop) [h : IsWellOrder α r] :

Cardinal.ord (Cardinal.mk α) ≤ Ordinal.type r

theorem Cardinal.ord_le {c : Cardinal.{u_3}} {o : Ordinal.{u_3}} :

Cardinal.ord c ≤ o ↔ c ≤ Ordinal.card o

theorem Cardinal.gc_ord_card :

GaloisConnection Cardinal.ord Ordinal.card

theorem Cardinal.lt_ord {c : Cardinal.{u_3}} {o : Ordinal.{u_3}} :

o < Cardinal.ord c ↔ Ordinal.card o < c

@[simp]

theorem Cardinal.card_ord (c : Cardinal.{u_3}) :

Ordinal.card (Cardinal.ord c) = c

def Cardinal.gciOrdCard :

GaloisCoinsertion Cardinal.ord Ordinal.card

Galois coinsertion between Cardinal.ord and Ordinal.card.

Equations

Cardinal.gciOrdCard = GaloisConnection.toGaloisCoinsertion Cardinal.gc_ord_card Cardinal.gciOrdCard.proof_1

Instances For

theorem Cardinal.ord_card_le (o : Ordinal.{u_3}) :

Cardinal.ord (Ordinal.card o) ≤ o

theorem Cardinal.lt_ord_succ_card (o : Ordinal.{u_3}) :

o < Cardinal.ord (Order.succ (Ordinal.card o))

theorem Cardinal.card_le_iff {o : Ordinal.{u_3}} {c : Cardinal.{u_3}} :

Ordinal.card o ≤ c ↔ o < Cardinal.ord (Order.succ c)

theorem Cardinal.card_le_of_le_ord {o : Ordinal.{u_3}} {c : Cardinal.{u_3}} (ho : o ≤ Cardinal.ord c) :

Ordinal.card o ≤ 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 = ℵ₀).

theorem Cardinal.ord_strictMono :

StrictMono Cardinal.ord

theorem Cardinal.ord_mono :

Monotone Cardinal.ord

@[simp]

theorem Cardinal.ord_le_ord {c₁ : Cardinal.{u_3}} {c₂ : Cardinal.{u_3}} :

Cardinal.ord c₁ ≤ Cardinal.ord c₂ ↔ c₁ ≤ c₂

@[simp]

theorem Cardinal.ord_lt_ord {c₁ : Cardinal.{u_3}} {c₂ : Cardinal.{u_3}} :

Cardinal.ord c₁ < Cardinal.ord c₂ ↔ c₁ < c₂

@[simp]

theorem Cardinal.ord_zero :

Cardinal.ord 0 = 0

@[simp]

theorem Cardinal.ord_nat (n : ℕ) :

Cardinal.ord ↑n = ↑n

@[simp]

theorem Cardinal.ord_one :

Cardinal.ord 1 = 1

@[simp]

theorem Cardinal.lift_ord (c : Cardinal.{v}) :

Ordinal.lift.{u, v} (Cardinal.ord c) = Cardinal.ord (Cardinal.lift.{u, v} c)

theorem Cardinal.mk_ord_out (c : Cardinal.{u_3}) :

Cardinal.mk (Quotient.out (Cardinal.ord c)).α = c

theorem Cardinal.card_typein_lt {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] (x : α) (h : Cardinal.ord (Cardinal.mk α) = Ordinal.type r) :

Ordinal.card (Ordinal.typein r x) < Cardinal.mk α

theorem Cardinal.card_typein_out_lt (c : Cardinal.{u_3}) (x : (Quotient.out (Cardinal.ord c)).α) :

Ordinal.card (Ordinal.typein (fun x x_1 => x < x_1) x) < c

theorem Cardinal.ord_injective :

Function.Injective Cardinal.ord

def Cardinal.ord.orderEmbedding :

Cardinal.{u_3} ↪o Ordinal.{u_3}

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.orderEmbedding = RelEmbedding.orderEmbeddingOfLTEmbedding (RelEmbedding.ofMonotone Cardinal.ord Cardinal.ord.orderEmbedding.proof_2)

Instances For

@[simp]

theorem Cardinal.ord.orderEmbedding_coe :

↑Cardinal.ord.orderEmbedding = Cardinal.ord

def Cardinal.univ :

Cardinal.{max (u + 1) v}

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.lift.{v, u + 1} (Cardinal.mk Ordinal.{u})

Instances For

theorem Cardinal.univ_id :

Cardinal.univ = Cardinal.mk Ordinal.{u}

@[simp]

theorem Cardinal.lift_univ :

Cardinal.lift.{w, max (u + 1) v} Cardinal.univ = Cardinal.univ

theorem Cardinal.univ_umax :

Cardinal.univ = Cardinal.univ

theorem Cardinal.lift_lt_univ (c : Cardinal.{u}) :

Cardinal.lift.{u + 1, u} c < Cardinal.univ

theorem Cardinal.lift_lt_univ' (c : Cardinal.{u}) :

Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ

@[simp]

theorem Cardinal.ord_univ :

Cardinal.ord Cardinal.univ = Ordinal.univ

theorem Cardinal.lt_univ {c : Cardinal.{u + 1} } :

c < Cardinal.univ ↔ ∃ c', c = Cardinal.lift.{u + 1, u} c'

theorem Cardinal.lt_univ' {c : Cardinal.{max (u + 1) v} } :

c < Cardinal.univ ↔ ∃ c', c = Cardinal.lift.{max (u + 1) v, u} c'

theorem Cardinal.small_iff_lift_mk_lt_univ {α : Type u} :

Small.{v, u} α ↔ Cardinal.lift.{v + 1, u} (Cardinal.mk α) < Cardinal.univ

@[simp]

theorem Ordinal.card_univ :

Ordinal.card Ordinal.univ = Cardinal.univ

@[simp]

theorem Ordinal.nat_le_card {o : Ordinal.{u_3}} {n : ℕ} :

↑n ≤ Ordinal.card o ↔ ↑n ≤ o

@[simp]

theorem Ordinal.nat_lt_card {o : Ordinal.{u_3}} {n : ℕ} :

↑n < Ordinal.card o ↔ ↑n < o

@[simp]

theorem Ordinal.card_lt_nat {o : Ordinal.{u_3}} {n : ℕ} :

Ordinal.card o < ↑n ↔ o < ↑n

@[simp]

theorem Ordinal.card_le_nat {o : Ordinal.{u_3}} {n : ℕ} :

Ordinal.card o ≤ ↑n ↔ o ≤ ↑n

@[simp]

theorem Ordinal.card_eq_nat {o : Ordinal.{u_3}} {n : ℕ} :

Ordinal.card o = ↑n ↔ o = ↑n

@[simp]

theorem Ordinal.type_fintype {α : Type u_3} (r : α → α → Prop) [IsWellOrder α r] [Fintype α] :

Ordinal.type r = ↑(Fintype.card α)

theorem Ordinal.type_fin (n : ℕ) :

(Ordinal.type fun x x_1 => x < x_1) = ↑n