# mathlib3documentation

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 #

noncomputable def embedding_to_cardinal {σ : Type u} :

An embedding of any type to the set of cardinals.

Equations
def well_ordering_rel {σ : Type u} :
σ σ Prop

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

Equations
Instances for `well_ordering_rel`
@[protected, instance]
@[protected, instance]
def is_well_order.subtype_nonempty {σ : Type u} :
nonempty {r // r}

### Definition of ordinals #

structure Well_order  :
Type (u+1)

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

Instances for `Well_order`
@[protected, instance]
Equations
@[simp]
theorem Well_order.eta (o : Well_order) :
{α := o.α, r := o.r, wo := _} = o
@[protected, instance]

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

Equations
def ordinal  :
Type (u+1)

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

Equations
Instances for `ordinal`
@[protected, instance]
Equations
@[protected, instance]
noncomputable def linear_order_out (o : ordinal) :
Equations
@[protected, instance]
def ordinal.type {α : Type u_1} (r : α α Prop) [wo : r] :

The order type of a well order is an ordinal.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def ordinal.typein {α : Type u_1} (r : α α Prop) [ r] (a : α) :

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

Equations
@[simp]
theorem ordinal.type_def' (w : Well_order) :
@[simp]
theorem ordinal.type_def {α : Type u_1} (r : α α Prop) [wo : r] :
{α := α, r := r, wo := wo} =
@[simp]
theorem ordinal.type_out (o : ordinal) :
= o
theorem ordinal.type_eq {α β : Type u_1} {r : α α Prop} {s : β β Prop} [ r] [ s] :
theorem rel_iso.ordinal_type_eq {α β : Type u_1} {r : α α Prop} {s : β β Prop} [ r] [ s] (h : r ≃r s) :
@[simp]
theorem ordinal.type_lt (o : ordinal) :
theorem ordinal.type_eq_zero_of_empty {α : Type u_1} (r : α α Prop) [ r] [is_empty α] :
@[simp]
theorem ordinal.type_eq_zero_iff_is_empty {α : Type u_1} {r : α α Prop} [ r] :
theorem ordinal.type_ne_zero_iff_nonempty {α : Type u_1} {r : α α Prop} [ r] :
theorem ordinal.type_ne_zero_of_nonempty {α : Type u_1} (r : α α Prop) [ r] [h : nonempty α] :
theorem ordinal.type_eq_one_of_unique {α : Type u_1} (r : α α Prop) [ r] [unique α] :
@[simp]
theorem ordinal.type_eq_one_iff_unique {α : Type u_1} {r : α α Prop} [ r] :
@[simp]
@[protected, instance]
@[simp]
@[protected]
theorem ordinal.one_ne_zero  :
1 0
@[protected, instance]
@[simp]
theorem ordinal.type_preimage {α β : Type u} (r : α α Prop) [ r] (f : β α) :
theorem ordinal.induction_on {C : ordinal Prop} (o : ordinal) (H : (α : Type u_1) (r : α α Prop) [_inst_1 : r], C (ordinal.type r)) :
C o

### The order on ordinals #

@[protected, instance]
Equations
• ordinal.partial_order = {le := λ (a b : ordinal), (λ (_x : Well_order), ordinal.partial_order._match_2 _x) ordinal.partial_order._proof_1, lt := λ (a b : ordinal), (λ (_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 s)
• ordinal.partial_order._match_11 α r {α := β, r := s, wo := wo'} = nonempty s)
theorem ordinal.type_le_iff {α β : Type u_1} {r : α α Prop} {s : β β Prop} [ r] [ s] :
theorem ordinal.type_le_iff' {α β : Type u_1} {r : α α Prop} {s : β β Prop} [ r] [ s] :
theorem initial_seg.ordinal_type_le {α β : Type u_1} {r : α α Prop} {s : β β Prop} [ r] [ s] (h : s) :
theorem rel_embedding.ordinal_type_le {α β : Type u_1} {r : α α Prop} {s : β β Prop} [ r] [ s] (h : r ↪r s) :
@[simp]
theorem ordinal.type_lt_iff {α β : Type u_1} {r : α α Prop} {s : β β Prop} [ r] [ s] :
theorem principal_seg.ordinal_type_lt {α β : Type u_1} {r : α α Prop} {s : β β Prop} [ r] [ s] (h : s) :
@[protected]
theorem ordinal.zero_le (o : ordinal) :
0 o
@[protected, instance]
Equations
@[simp]
theorem ordinal.bot_eq_zero  :
= 0
@[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]
Equations
@[protected, instance]
noncomputable def ordinal.initial_seg_out {α β : ordinal} (h : α β) :

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

Equations
noncomputable def ordinal.principal_seg_out {α β : ordinal} (h : α < β) :

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

Equations
theorem ordinal.typein_lt_type {α : Type u_1} (r : α α Prop) [ r] (a : α) :
theorem ordinal.typein_lt_self {o : ordinal} (i : (quotient.out o).α) :
@[simp]
theorem ordinal.typein_top {α β : Type u_1} {r : α α Prop} {s : β β Prop} [ r] [ s] (f : s) :
@[simp]
theorem ordinal.typein_apply {α β : Type u_1} {r : α α Prop} {s : β β Prop} [ r] [ s] (f : s) (a : α) :
(f a) =
@[simp]
theorem ordinal.typein_lt_typein {α : Type u_1} (r : α α Prop) [ r] {a b : α} :
< r a b
theorem ordinal.typein_surj {α : Type u_1} (r : α α Prop) [ r] {o : ordinal} (h : o < ) :
(a : α), = o
theorem ordinal.typein_injective {α : Type u_1} (r : α α Prop) [ r] :
@[simp]
theorem ordinal.typein_inj {α : Type u_1} (r : α α Prop) [ r] {a b : α} :
= a = b
def ordinal.typein.principal_seg {α : Type u_1} (r : α α Prop) [ r] :

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

Equations
@[simp]
theorem ordinal.typein.principal_seg_coe {α : Type u_1} (r : α α Prop) [ r] :

### Enumerating elements in a well-order with ordinals. #

noncomputable def ordinal.enum {α : Type u_1} (r : α α Prop) [ r] (o : ordinal) (h : o < ) :
α

`enum r o h` is the `o`-th element of `α` ordered by `r`. That is, `enum` maps an initial segment of the ordinals, those less than the order type of `r`, to the elements of `α`.

Equations
theorem ordinal.enum_type {α β : Type u_1} {r : α α Prop} {s : β β Prop} [ r] [ s] (f : r) {h : < } :
(ordinal.type s) h = f.top
@[simp]
theorem ordinal.enum_typein {α : Type u_1} (r : α α Prop) [ r] (a : α) :
a) _ = a
@[simp]
theorem ordinal.typein_enum {α : Type u_1} (r : α α Prop) [ r] {o : ordinal} (h : o < ) :
o h) = o
theorem ordinal.enum_lt_enum {α : Type u_1} {r : α α Prop} [ r] {o₁ o₂ : ordinal} (h₁ : o₁ < ) (h₂ : o₂ < ) :
r o₁ h₁) o₂ h₂) o₁ < o₂
theorem ordinal.rel_iso_enum' {α β : Type u} {r : α α Prop} {s : β β Prop} [ r] [ s] (f : r ≃r s) (o : ordinal) (hr : o < ) (hs : o < ) :
f o hr) = o hs
theorem ordinal.rel_iso_enum {α β : Type u} {r : α α Prop} {s : β β Prop} [ r] [ s] (f : r ≃r s) (o : ordinal) (hr : o < ) :
f o hr) = o _
theorem ordinal.lt_wf  :
@[protected, instance]
Equations
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`.

### 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
@[simp]
theorem ordinal.card_type {α : Type u_1} (r : α α Prop) [ r] :
@[simp]
theorem ordinal.card_typein {α : Type u_1} {r : α α Prop} [wo : r] (x : α) :
cardinal.mk {y // r y x} = 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 #

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
@[simp]
theorem ordinal.type_ulift {α : Type u_1} (r : α α Prop) [ r] :
theorem rel_iso.ordinal_lift_type_eq {α : Type u} {β : Type v} {r : α α Prop} {s : β β Prop} [ r] [ s] (f : r ≃r s) :
@[simp]
theorem ordinal.type_lift_preimage {α : Type u} {β : Type v} (r : α α Prop) [ r] (f : β α) :
@[simp]

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

`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) :
theorem ordinal.lift_type_le {α : Type u} {β : Type v} {r : α α Prop} {s : β β Prop} [ r] [ s] :
theorem ordinal.lift_type_eq {α : Type u} {β : Type v} {r : α α Prop} {s : β β Prop} [ r] [ s] :
theorem ordinal.lift_type_lt {α : Type u} {β : Type v} {r : α α Prop} {s : β β Prop} [ 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) :
theorem ordinal.lift_down' {a : cardinal} {b : ordinal} (h : b.card a.lift) :
(a' : ordinal), a'.lift = b
theorem ordinal.lift_down {a : ordinal} {b : ordinal} (h : b a.lift) :
(a' : ordinal), a'.lift = b
theorem ordinal.le_lift_iff {a : ordinal} {b : ordinal} :
b a.lift (a' : ordinal), a'.lift = b a' a
theorem ordinal.lt_lift_iff {a : ordinal} {b : ordinal} :
b < a.lift (a' : ordinal), a'.lift = b a' < a

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

Equations
@[simp]

### The first infinite ordinal `omega`#

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

Equations
@[simp]

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 `ordinal_arithmetic.lean`.

@[protected, instance]

`o₁ + o₂` is the order on the disjoint union of `o₁` and `o₂` obtained by declaring that every element of `o₁` is smaller than every element of `o₂`.

Equations
@[protected, instance]
Equations
@[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) [ r] [ s] :
@[simp]
theorem ordinal.card_nat (n : ) :
@[protected, instance]
@[protected, instance]
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  :
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[simp]
theorem ordinal.max_zero_left (a : ordinal) :
= a
@[simp]
theorem ordinal.max_zero_right (a : ordinal) :
= a
@[simp]
theorem ordinal.max_eq_zero {a b : ordinal} :
= 0 a = 0 b = 0
@[simp]
theorem ordinal.Inf_empty  :
@[protected, instance]
@[protected, instance]
noncomputable def ordinal.succ_order  :
Equations
@[simp]
theorem ordinal.add_one_eq_succ (o : ordinal) :
o + 1 =
@[simp]
theorem ordinal.succ_zero  :
= 1
@[simp]
theorem ordinal.succ_one  :
= 2
theorem ordinal.add_succ (o₁ o₂ : ordinal) :
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 <
theorem ordinal.succ_ne_zero (o : ordinal) :
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) :
theorem ordinal.nat_cast_succ (n : ) :
(n.succ) =
@[protected, instance]
Equations
@[protected, instance]
noncomputable def ordinal.unique_out_one  :
Equations
theorem ordinal.one_out_eq (x : (quotient.out 1).α) :
x =

### Extra properties of typein and enum #

@[simp]
theorem ordinal.typein_one_out (x : (quotient.out 1).α) :
@[simp]
theorem ordinal.typein_le_typein {α : Type u_1} (r : α α Prop) [ r] {x x' : α} :
x' ¬r x' x
@[simp]
theorem ordinal.typein_le_typein' (o : ordinal) {x x' : (quotient.out o).α} :
x x'
@[simp]
theorem ordinal.enum_le_enum {α : Type u_1} (r : α α Prop) [ r] {o o' : ordinal} (ho : o < ) (ho' : o' < ) :
¬r o' ho') o ho) o o'
@[simp]
theorem ordinal.enum_le_enum' (a : ordinal) {o o' : ordinal} (ho : o < ) (ho' : o' < ) :
ho' o o'
theorem ordinal.enum_zero_le {α : Type u_1} {r : α α Prop} [ r] (h0 : 0 < ) (a : α) :
¬r a 0 h0)
theorem ordinal.enum_zero_le' {o : ordinal} (h0 : 0 < o) (a : (quotient.out o).α) :
a
@[simp]
theorem ordinal.enum_inj {α : Type u_1} {r : α α Prop} [ r] {o₁ o₂ : ordinal} (h₁ : o₁ < ) (h₂ : o₂ < ) :
o₁ h₁ = o₂ h₂ o₁ = o₂
noncomputable def ordinal.enum_iso {α : Type u_1} (r : α α Prop) [ r] :
(λ (_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
@[simp]
theorem ordinal.enum_iso_apply {α : Type u_1} (r : α α Prop) [ r] (x : (λ (_x : ordinal), _x < ordinal.type r)) :
x = x.val _
@[simp]
theorem ordinal.enum_iso_symm_apply_coe {α : Type u_1} (r : α α Prop) [ r] (x : α) :
@[simp]
noncomputable def ordinal.enum_iso_out (o : ordinal) :

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

Equations
noncomputable def ordinal.out_order_bot_of_pos {o : ordinal} (ho : 0 < o) :

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

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

### Universal ordinal #

@[nolint]

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

Equations
@[simp]

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

Equations
@[simp]
@[simp]

### Representing a cardinal with an ordinal #

@[simp]
theorem cardinal.mk_ordinal_out (o : ordinal) :
= 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), (r : {r // r}), in F cardinal.ord._proof_2
theorem cardinal.ord_eq_Inf (α : Type u) :
(cardinal.mk α).ord = (r : {r // r}),
theorem cardinal.ord_eq (α : Type u_1) :
(r : α α Prop) [wo : r], (cardinal.mk α).ord =
theorem cardinal.ord_le_type {α : Type u_1} (r : α α Prop) [h : r] :
theorem cardinal.ord_le {c : cardinal} {o : ordinal} :
c.ord o c o.card
theorem cardinal.lt_ord {c : cardinal} {o : ordinal} :
o < c.ord o.card < c
@[simp]
theorem cardinal.card_ord (c : cardinal) :
c.ord.card = c
noncomputable def cardinal.gci_ord_card  :

Galois coinsertion between `cardinal.ord` and `ordinal.card`.

Equations
@[simp]
theorem cardinal.ord_le_ord {c₁ c₂ : cardinal} :
c₁.ord c₂.ord c₁ c₂
@[simp]
theorem cardinal.ord_lt_ord {c₁ c₂ : cardinal} :
c₁.ord < c₂.ord c₁ < c₂
@[simp]
theorem cardinal.ord_zero  :
0.ord = 0
@[simp]
theorem cardinal.ord_nat (n : ) :
@[simp]
theorem cardinal.ord_one  :
1.ord = 1
@[simp]
theorem cardinal.lift_ord (c : cardinal) :
theorem cardinal.mk_ord_out (c : cardinal) :
= c
theorem cardinal.card_typein_lt {α : Type u_1} (r : α α Prop) [ r] (x : α) (h : (cardinal.mk α).ord = ) :
x).card <
noncomputable def cardinal.ord.order_embedding  :

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

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

Equations
@[simp]
@[simp]
theorem cardinal.lt_univ {c : cardinal} :
(c' : cardinal), c = c'.lift
theorem cardinal.lt_univ' {c : cardinal} :
(c' : cardinal), c = c'.lift
@[simp]
@[simp]
theorem ordinal.nat_le_card {o : ordinal} {n : } :
@[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 : } :
@[simp]
theorem ordinal.card_eq_nat {o : ordinal} {n : } :
o.card = n o = n
@[simp]
theorem ordinal.type_fintype {α : Type u_1} (r : α α Prop) [ r] [fintype α] :
theorem ordinal.type_fin (n : ) :