# mathlibdocumentation

set_theory.ordinal_arithmetic

# Ordinal arithmetic #

Ordinals have an addition (corresponding to disjoint union) that turns them into an additive monoid, and a multiplication (corresponding to the lexicographic order on the product) that turns them into a monoid. One can also define correspondingly a subtraction, a division, a successor function, a power function and a logarithm function.

We also define limit ordinals and prove the basic induction principle on ordinals separating successor ordinals and limit ordinals, in `limit_rec_on`.

## Main definitions and results #

• `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₂`.
• `o₁ - o₂` is the unique ordinal `o` such that `o₂ + o = o₁`, when `o₂ ≤ o₁`.
• `o₁ * o₂` is the lexicographic order on `o₂ × o₁`.
• `o₁ / o₂` is the ordinal `o` such that `o₁ = o₂ * o + o'` with `o' < o₂`. We also define the divisibility predicate, and a modulo operation.
• `succ o = o + 1` is the successor of `o`.
• `pred o` if the predecessor of `o`. If `o` is not a successor, we set `pred o = o`.

We also define the power function and the logarithm function on ordinals, and discuss the properties of casts of natural numbers of and of `omega` with respect to these operations.

Some properties of the operations are also used to discuss general tools on ordinals:

• `is_limit o`: an ordinal is a limit ordinal if it is neither `0` nor a successor.
• `limit_rec_on` is the main induction principle of ordinals: if one can prove a property by induction at successor ordinals and at limit ordinals, then it holds for all ordinals.
• `is_normal`: a function `f : ordinal → ordinal` satisfies `is_normal` if it is strictly increasing and order-continuous, i.e., the image `f o` of a limit ordinal `o` is the sup of `f a` for `a < o`.
• `enum_ord`: enumerates an unbounded set of ordinals by the ordinals themselves.
• `nfp f a`: the next fixed point of a function `f` on ordinals, above `a`. It behaves well for normal functions.
• `CNF b o` is the Cantor normal form of the ordinal `o` in base `b`.
• `sup`, `lsub`: the supremum / least strict upper bound of an indexed family of ordinals in `Type u`, as an ordinal in `Type u`.
• `bsup`, `blsub`: the supremum / least strict upper bound of a set of ordinals indexed by ordinals less than a given ordinal `o`.

### Further properties of addition on ordinals #

@[simp]
theorem ordinal.lift_add (a b : ordinal) :
(a + b).lift = a.lift + b.lift
@[simp]
theorem ordinal.lift_succ (a : ordinal) :
a + b a + c b c
theorem ordinal.add_succ (o₁ o₂ : ordinal) :
o₁ + o₂.succ = (o₁ + o₂).succ
@[simp]
theorem ordinal.succ_zero  :
0.succ = 1
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 < o.succ
theorem ordinal.succ_ne_zero (o : ordinal) :
o.succ 0
@[simp]
theorem ordinal.card_succ (o : ordinal) :
o.succ.card = o.card + 1
theorem ordinal.nat_cast_succ (n : ) :
theorem ordinal.add_left_cancel (a : ordinal) {b c : ordinal} :
a + b = a + c b = c
theorem ordinal.lt_succ {a b : ordinal} :
a < b.succ a b
theorem ordinal.lt_one_iff_zero {a : ordinal} :
a < 1 a = 0
a + b < a + c b < c
a + b < c + ba < c
@[simp]
theorem ordinal.succ_lt_succ {a b : ordinal} :
a.succ < b.succ a < b
@[simp]
theorem ordinal.succ_le_succ {a b : ordinal} :
a.succ b.succ a b
theorem ordinal.succ_inj {a b : ordinal} :
a.succ = b.succ a = b
a + n b + n a b
theorem ordinal.add_right_cancel {a b : ordinal} (n : ) :
a + n = b + n a = b

### The zero ordinal #

@[simp]
theorem ordinal.card_eq_zero {o : ordinal} :
o.card = 0 o = 0
@[simp]
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] :
@[protected]
theorem ordinal.one_ne_zero  :
1 0
@[protected, instance]
theorem ordinal.zero_lt_one  :
0 < 1

### The predecessor of an ordinal #

noncomputable def ordinal.pred (o : ordinal) :

The ordinal predecessor of `o` is `o'` if `o = succ o'`, and `o` otherwise.

Equations
@[simp]
theorem ordinal.pred_succ (o : ordinal) :
o.succ.pred = o
theorem ordinal.pred_le_self (o : ordinal) :
o.pred o
theorem ordinal.pred_eq_iff_not_succ {o : ordinal} :
o.pred = o ¬∃ (a : ordinal), o = a.succ
theorem ordinal.pred_lt_iff_is_succ {o : ordinal} :
o.pred < o ∃ (a : ordinal), o = a.succ
theorem ordinal.succ_pred_iff_is_succ {o : ordinal} :
o.pred.succ = o ∃ (a : ordinal), o = a.succ
theorem ordinal.succ_lt_of_not_succ {o : ordinal} (h : ¬∃ (a : ordinal), o = a.succ) {b : ordinal} :
b.succ < o b < o
theorem ordinal.lt_pred {a b : ordinal} :
a < b.pred a.succ < b
theorem ordinal.pred_le {a b : ordinal} :
a.pred b a b.succ
@[simp]
theorem ordinal.lift_is_succ {o : ordinal} :
(∃ (a : ordinal), o.lift = a.succ) ∃ (a : ordinal), o = a.succ
@[simp]
theorem ordinal.lift_pred (o : ordinal) :

### Limit ordinals #

def ordinal.is_limit (o : ordinal) :
Prop

A limit ordinal is an ordinal which is not zero and not a successor.

Equations
theorem ordinal.not_succ_of_is_limit {o : ordinal} (h : o.is_limit) :
¬∃ (a : ordinal), o = a.succ
theorem ordinal.succ_lt_of_is_limit {o : ordinal} (h : o.is_limit) {a : ordinal} :
a.succ < o a < o
theorem ordinal.le_succ_of_is_limit {o : ordinal} (h : o.is_limit) {a : ordinal} :
o a.succ o a
theorem ordinal.limit_le {o : ordinal} (h : o.is_limit) {a : ordinal} :
o a ∀ (x : ordinal), x < ox a
theorem ordinal.lt_limit {o : ordinal} (h : o.is_limit) {a : ordinal} :
a < o ∃ (x : ordinal) (H : x < o), a < x
@[simp]
theorem ordinal.lift_is_limit (o : ordinal) :
theorem ordinal.is_limit.pos {o : ordinal} (h : o.is_limit) :
0 < o
theorem ordinal.is_limit.one_lt {o : ordinal} (h : o.is_limit) :
1 < o
theorem ordinal.is_limit.nat_lt {o : ordinal} (h : o.is_limit) (n : ) :
n < o
theorem ordinal.zero_or_succ_or_limit (o : ordinal) :
o = 0 (∃ (a : ordinal), o = a.succ) o.is_limit
noncomputable def ordinal.limit_rec_on {C : ordinalSort u_2} (o : ordinal) (H₁ : C 0) (H₂ : Π (o : ordinal), C oC o.succ) (H₃ : Π (o : ordinal), o.is_limit(Π (o' : ordinal), o' < oC o')C o) :
C o

Main induction principle of ordinals: if one can prove a property by induction at successor ordinals and at limit ordinals, then it holds for all ordinals.

Equations
@[simp]
theorem ordinal.limit_rec_on_zero {C : ordinalSort u_2} (H₁ : C 0) (H₂ : Π (o : ordinal), C oC o.succ) (H₃ : Π (o : ordinal), o.is_limit(Π (o' : ordinal), o' < oC o')C o) :
0.limit_rec_on H₁ H₂ H₃ = H₁
@[simp]
theorem ordinal.limit_rec_on_succ {C : ordinalSort u_2} (o : ordinal) (H₁ : C 0) (H₂ : Π (o : ordinal), C oC o.succ) (H₃ : Π (o : ordinal), o.is_limit(Π (o' : ordinal), o' < oC o')C o) :
o.succ.limit_rec_on H₁ H₂ H₃ = H₂ o (o.limit_rec_on H₁ H₂ H₃)
@[simp]
theorem ordinal.limit_rec_on_limit {C : ordinalSort u_2} (o : ordinal) (H₁ : C 0) (H₂ : Π (o : ordinal), C oC o.succ) (H₃ : Π (o : ordinal), o.is_limit(Π (o' : ordinal), o' < oC o')C o) (h : o.is_limit) :
o.limit_rec_on H₁ H₂ H₃ = H₃ o h (λ (x : ordinal) (h : x < o), x.limit_rec_on H₁ H₂ H₃)
theorem ordinal.has_succ_of_is_limit {α : Type u_1} {r : α → α → Prop} [wo : r] (h : (ordinal.type r).is_limit) (x : α) :
∃ (y : α), r x y
theorem ordinal.type_subrel_lt (o : ordinal) :
ordinal.type {o' : ordinal | o' < o}) = o.lift
theorem ordinal.mk_initial_seg (o : ordinal) :
# {o' : ordinal | o' < o} = o.card.lift

### Normal ordinal functions #

def ordinal.is_normal (f : ordinalordinal) :
Prop

A normal ordinal function is a strictly increasing function which is order-continuous, i.e., the image `f o` of a limit ordinal `o` is the sup of `f a` for `a < o`.

Equations
theorem ordinal.is_normal.limit_le {f : ordinalordinal} (H : ordinal.is_normal f) {o : ordinal} :
o.is_limit∀ {a : ordinal}, f o a ∀ (b : ordinal), b < of b a
theorem ordinal.is_normal.limit_lt {f : ordinalordinal} (H : ordinal.is_normal f) {o : ordinal} (h : o.is_limit) {a : ordinal} :
a < f o ∃ (b : ordinal) (H : b < o), a < f b
theorem ordinal.is_normal.lt_iff {f : ordinalordinal} (H : ordinal.is_normal f) {a b : ordinal} :
f a < f b a < b
theorem ordinal.is_normal.le_iff {f : ordinalordinal} (H : ordinal.is_normal f) {a b : ordinal} :
f a f b a b
theorem ordinal.is_normal.inj {f : ordinalordinal} (H : ordinal.is_normal f) {a b : ordinal} :
f a = f b a = b
theorem ordinal.is_normal.le_self {f : ordinalordinal} (H : ordinal.is_normal f) (a : ordinal) :
a f a
theorem ordinal.is_normal.le_set {f : ordinalordinal} (H : ordinal.is_normal f) (p : ordinal → Prop) (p0 : ∃ (x : ordinal), p x) (S : ordinal) (H₂ : ∀ (o : ordinal), S o ∀ (a : ordinal), p aa o) {o : ordinal} :
f S o ∀ (a : ordinal), p af a o
theorem ordinal.is_normal.le_set' {α : Type u_1} {f : ordinalordinal} (H : ordinal.is_normal f) (p : α → Prop) (g : α → ordinal) (p0 : ∃ (x : α), p x) (S : ordinal) (H₂ : ∀ (o : ordinal), S o ∀ (a : α), p ag a o) {o : ordinal} :
f S o ∀ (a : α), p af (g a) o
theorem ordinal.is_normal.trans {f : ordinalordinal} {g : ordinalordinal} (H₁ : ordinal.is_normal f) (H₂ : ordinal.is_normal g) :
ordinal.is_normal (λ (x : ordinal), f (g x))
theorem ordinal.is_normal.is_limit {f : ordinalordinal} (H : ordinal.is_normal f) {o : ordinal} (l : o.is_limit) :
(f o).is_limit
theorem ordinal.add_le_of_limit {a b c : ordinal} (h : b.is_limit) :
a + b c ∀ (b' : ordinal), b' < ba + b' c
theorem ordinal.add_is_limit (a : ordinal) {b : ordinal} :
b.is_limit(a + b).is_limit

### Subtraction on ordinals #

noncomputable def ordinal.sub (a b : ordinal) :

`a - b` is the unique ordinal satisfying `b + (a - b) = a` when `b ≤ a`.

Equations
@[protected, instance]
noncomputable def ordinal.has_sub  :
Equations
theorem ordinal.le_add_sub (a b : ordinal) :
a b + (a - b)
theorem ordinal.sub_le {a b c : ordinal} :
a - b c a b + c
theorem ordinal.lt_sub {a b c : ordinal} :
a < b - c c + a < b
theorem ordinal.add_sub_cancel (a b : ordinal) :
a + b - a = b
theorem ordinal.sub_eq_of_add_eq {a b c : ordinal} (h : a + b = c) :
c - a = b
theorem ordinal.sub_le_self (a b : ordinal) :
a - b a
@[protected]
theorem ordinal.add_sub_cancel_of_le {a b : ordinal} (h : b a) :
b + (a - b) = a
@[simp]
theorem ordinal.sub_zero (a : ordinal) :
a - 0 = a
@[simp]
theorem ordinal.zero_sub (a : ordinal) :
0 - a = 0
@[simp]
theorem ordinal.sub_self (a : ordinal) :
a - a = 0
@[protected]
theorem ordinal.sub_eq_zero_iff_le {a b : ordinal} :
a - b = 0 a b
theorem ordinal.sub_sub (a b c : ordinal) :
a - b - c = a - (b + c)
a + b - (a + c) = b - c
theorem ordinal.sub_is_limit {a b : ordinal} (l : a.is_limit) (h : b < a) :
(a - b).is_limit
@[simp]
1 + ω = ω
@[simp]
theorem ordinal.one_add_of_omega_le {o : ordinal} (h : ω o) :
1 + o = o

### Multiplication of ordinals #

@[protected, instance]

The multiplication of ordinals `o₁` and `o₂` is the (well founded) lexicographic order on `o₂ × o₁`.

Equations
@[simp]
theorem ordinal.type_mul {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [ r] [ s] :
@[simp]
theorem ordinal.lift_mul (a b : ordinal) :
(a * b).lift = (a.lift) * b.lift
@[simp]
theorem ordinal.card_mul (a b : ordinal) :
(a * b).card = (a.card) * b.card
@[simp]
theorem ordinal.mul_zero (a : ordinal) :
a * 0 = 0
@[simp]
theorem ordinal.zero_mul (a : ordinal) :
0 * a = 0
theorem ordinal.mul_add (a b c : ordinal) :
a * (b + c) = a * b + a * c
@[simp]
theorem ordinal.mul_add_one (a b : ordinal) :
a * (b + 1) = a * b + a
@[simp]
theorem ordinal.mul_succ (a b : ordinal) :
a * b.succ = a * b + a
theorem ordinal.mul_le_mul_left {a b : ordinal} (c : ordinal) :
a bc * a c * b
theorem ordinal.mul_le_mul_right {a b : ordinal} (c : ordinal) :
a ba * c b * c
theorem ordinal.le_mul_left (a : ordinal) {b : ordinal} (hb : 0 < b) :
a a * b
theorem ordinal.le_mul_right (a : ordinal) {b : ordinal} (hb : 0 < b) :
a b * a
theorem ordinal.mul_le_mul {a b c d : ordinal} (h₁ : a c) (h₂ : b d) :
a * b c * d
theorem ordinal.mul_le_of_limit {a b c : ordinal} (h : b.is_limit) :
a * b c ∀ (b' : ordinal), b' < ba * b' c
theorem ordinal.mul_is_normal {a : ordinal} (h : 0 < a) :
theorem ordinal.lt_mul_of_limit {a b c : ordinal} (h : c.is_limit) :
a < b * c ∃ (c' : ordinal) (H : c' < c), a < b * c'
theorem ordinal.mul_lt_mul_iff_left {a b c : ordinal} (a0 : 0 < a) :
a * b < a * c b < c
theorem ordinal.mul_le_mul_iff_left {a b c : ordinal} (a0 : 0 < a) :
a * b a * c b c
theorem ordinal.mul_lt_mul_of_pos_left {a b c : ordinal} (h : a < b) (c0 : 0 < c) :
c * a < c * b
theorem ordinal.mul_pos {a b : ordinal} (h₁ : 0 < a) (h₂ : 0 < b) :
0 < a * b
theorem ordinal.mul_ne_zero {a b : ordinal} :
a 0b 0a * b 0
theorem ordinal.le_of_mul_le_mul_left {a b c : ordinal} (h : c * a c * b) (h0 : 0 < c) :
a b
theorem ordinal.mul_right_inj {a b c : ordinal} (a0 : 0 < a) :
a * b = a * c b = c
theorem ordinal.mul_is_limit {a b : ordinal} (a0 : 0 < a) :
b.is_limit(a * b).is_limit
theorem ordinal.mul_is_limit_left {a b : ordinal} (l : a.is_limit) (b0 : 0 < b) :
(a * b).is_limit

### Division on ordinals #

@[protected]
theorem ordinal.div_aux (a b : ordinal) (h : b 0) :
{o : ordinal | a < b * o.succ}.nonempty
@[protected]
noncomputable def ordinal.div (a b : ordinal) :

`a / b` is the unique ordinal `o` satisfying `a = b * o + o'` with `o' < b`.

Equations
@[protected, instance]
noncomputable def ordinal.has_div  :
Equations
@[simp]
theorem ordinal.div_zero (a : ordinal) :
a / 0 = 0
theorem ordinal.div_def (a : ordinal) {b : ordinal} (h : b 0) :
a / b = ordinal.omin {o : ordinal | a < b * o.succ} _
theorem ordinal.lt_mul_succ_div (a : ordinal) {b : ordinal} (h : b 0) :
a < b * (a / b).succ
theorem ordinal.lt_mul_div_add (a : ordinal) {b : ordinal} (h : b 0) :
a < b * (a / b) + b
theorem ordinal.div_le {a b c : ordinal} (b0 : b 0) :
a / b c a < b * c.succ
theorem ordinal.lt_div {a b c : ordinal} (c0 : c 0) :
a < b / c c * a.succ b
theorem ordinal.le_div {a b c : ordinal} (c0 : c 0) :
a b / c c * a b
theorem ordinal.div_lt {a b c : ordinal} (b0 : b 0) :
a / b < c a < b * c
theorem ordinal.div_le_of_le_mul {a b c : ordinal} (h : a b * c) :
a / b c
theorem ordinal.mul_lt_of_lt_div {a b c : ordinal} :
a < b / cc * a < b
@[simp]
theorem ordinal.zero_div (a : ordinal) :
0 / a = 0
theorem ordinal.mul_div_le (a b : ordinal) :
b * (a / b) a
theorem ordinal.mul_add_div (a : ordinal) {b : ordinal} (b0 : b 0) (c : ordinal) :
(b * a + c) / b = a + c / b
theorem ordinal.div_eq_zero_of_lt {a b : ordinal} (h : a < b) :
a / b = 0
@[simp]
theorem ordinal.mul_div_cancel (a : ordinal) {b : ordinal} (b0 : b 0) :
b * a / b = a
@[simp]
theorem ordinal.div_one (a : ordinal) :
a / 1 = a
@[simp]
theorem ordinal.div_self {a : ordinal} (h : a 0) :
a / a = 1
theorem ordinal.mul_sub (a b c : ordinal) :
a * (b - c) = a * b - a * c
theorem ordinal.dvd_add_iff {a b c : ordinal} :
a b(a b + c a c)
theorem ordinal.dvd_add {a b c : ordinal} (h₁ : a b) :
a ca b + c
theorem ordinal.dvd_zero (a : ordinal) :
a 0
theorem ordinal.zero_dvd {a : ordinal} :
0 a a = 0
theorem ordinal.one_dvd (a : ordinal) :
1 a
theorem ordinal.div_mul_cancel {a b : ordinal} :
a 0a ba * (b / a) = b
theorem ordinal.le_of_dvd {a b : ordinal} :
b 0a ba b
theorem ordinal.dvd_antisymm {a b : ordinal} (h₁ : a b) (h₂ : b a) :
a = b
@[protected, instance]
noncomputable def ordinal.has_mod  :

`a % b` is the unique ordinal `o'` satisfying `a = b * o + o'` with `o' < b`.

Equations
theorem ordinal.mod_def (a b : ordinal) :
a % b = a - b * (a / b)
@[simp]
theorem ordinal.mod_zero (a : ordinal) :
a % 0 = a
theorem ordinal.mod_eq_of_lt {a b : ordinal} (h : a < b) :
a % b = a
@[simp]
theorem ordinal.zero_mod (b : ordinal) :
0 % b = 0
theorem ordinal.div_add_mod (a b : ordinal) :
b * (a / b) + a % b = a
theorem ordinal.mod_lt (a : ordinal) {b : ordinal} (h : b 0) :
a % b < b
@[simp]
theorem ordinal.mod_self (a : ordinal) :
a % a = 0
@[simp]
theorem ordinal.mod_one (a : ordinal) :
a % 1 = 0
theorem ordinal.dvd_of_mod_eq_zero {a b : ordinal} (H : a % b = 0) :
b a
theorem ordinal.mod_eq_zero_of_dvd {a b : ordinal} (H : b a) :
a % b = 0
theorem ordinal.dvd_iff_mod_eq_zero {a b : ordinal} :
b a a % b = 0

### Families of ordinals #

There are two kinds of indexed families that naturally arise when dealing with ordinals: those indexed by some type in the appropriate universe, and those indexed by ordinals less than another. The following API allows one to convert from one kind of family to the other.

In many cases, this makes it easy to prove claims about one kind of family via the corresponding claim on the other.

noncomputable def ordinal.bfamily_of_family' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [ r] (f : ι → α) (a : ordinal) (H : a < ) :
α

Converts a family indexed by a `Type u` to one indexed by an `ordinal.{u}` using a specified well-ordering.

Equations
noncomputable def ordinal.bfamily_of_family {α : Type u_1} {ι : Type u} :
(ι → α)Π (a : ordinal),

Converts a family indexed by a `Type u` to one indexed by an `ordinal.{u}` using a well-ordering given by the axiom of choice.

Equations
def ordinal.family_of_bfamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [ r] {o : ordinal} (ho : = o) (f : Π (a : ordinal), a < o → α) :
ι → α

Converts a family indexed by an `ordinal.{u}` to one indexed by an `Type u` using a specified well-ordering.

Equations
• = λ (i : ι), f i) _
def ordinal.family_of_bfamily {α : Type u_1} (o : ordinal) (f : Π (a : ordinal), a < o → α) :
(quotient.out o).α → α

Converts a family indexed by an `ordinal.{u}` to one indexed by a `Type u` using a well-ordering given by the axiom of choice.

Equations
@[simp]
theorem ordinal.bfamily_of_family'_typein {α : Type u_1} {ι : Type u_2} (r : ι → ι → Prop) [ r] (f : ι → α) (i : ι) :
i) _ = f i
@[simp]
theorem ordinal.bfamily_of_family_typein {α : Type u_1} {ι : Type u_2} (f : ι → α) (i : ι) :
@[simp]
theorem ordinal.family_of_bfamily'_enum {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [ r] {o : ordinal} (ho : = o) (f : Π (a : ordinal), a < o → α) (i : ordinal) (hi : i < o) :
i _) = f i hi
@[simp]
theorem ordinal.family_of_bfamily_enum {α : Type u_1} (o : ordinal) (f : Π (a : ordinal), a < o → α) (i : ordinal) (hi : i < o) :
i _) = f i hi

### Supremum of a family of ordinals #

noncomputable def ordinal.sup {ι : Type u_1} (f : ι → ordinal) :

The supremum of a family of ordinals

Equations
theorem ordinal.le_sup {ι : Type u_1} (f : ι → ordinal) (i : ι) :
f i
theorem ordinal.sup_le {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
a ∀ (i : ι), f i a
theorem ordinal.lt_sup {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
a < ∃ (i : ι), a < f i
theorem ordinal.lt_sup_of_ne_sup {ι : Type u_1} {f : ι → ordinal} :
(∀ (i : ι), f i ∀ (i : ι), f i <
theorem ordinal.sup_not_succ_of_ne_sup {ι : Type u_1} {f : ι → ordinal} (hf : ∀ (i : ι), f i ) {a : ordinal} (hao : a < ) :
a.succ <
@[simp]
theorem ordinal.sup_eq_zero_iff {ι : Type u_1} {f : ι → ordinal} :
= 0 ∀ (i : ι), f i = 0
theorem ordinal.is_normal.sup {f : ordinalordinal} (H : ordinal.is_normal f) {ι : Type u_1} {g : ι → ordinal} (h : nonempty ι) :
theorem ordinal.sup_ord {ι : Type u_1} (f : ι → cardinal) :
ordinal.sup (λ (i : ι), (f i).ord) = (cardinal.sup f).ord
theorem ordinal.unbounded_range_of_sup_ge {α β : Type u} (r : α → α → Prop) [ r] (f : β → α) (h : ordinal.sup f)) :
noncomputable def ordinal.bsup (o : ordinal) :
(Π (a : ordinal), a < oordinal)ordinal

The supremum of a family of ordinals indexed by the set of ordinals less than some `o : ordinal.{u}`. (This is not a special case of `sup` over the subtype, because `{a // a < o} : Type (u+1)` and `sup` only works over families in `Type u`.)

Equations
theorem ordinal.bsup_le {o : ordinal} {f : Π (a : ordinal), a < oordinal} {a : ordinal} :
o.bsup f a ∀ (i : ordinal) (h : i < o), f i h a
theorem ordinal.le_bsup {o : ordinal} (f : Π (a : ordinal), a < oordinal) (i : ordinal) (h : i < o) :
f i h o.bsup f
theorem ordinal.lt_bsup {o : ordinal} (f : Π (a : ordinal), a < oordinal) {a : ordinal} :
a < o.bsup f ∃ (i : ordinal) (hi : i < o), a < f i hi
theorem ordinal.bsup_eq_sup' {o : ordinal} {ι : Type u_1} (r : ι → ι → Prop) [ r] (ho : = o) (f : Π (a : ordinal), a < oordinal) :
o.bsup f =
theorem ordinal.sup_eq_sup {ι : Type u} (r r' : ι → ι → Prop) [ r] [ r'] {o : ordinal} (ho : = o) (ho' : = o) (f : Π (a : ordinal), a < oordinal) :
= ordinal.sup ho' f)
theorem ordinal.bsup_eq_sup {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
o.bsup f =
theorem ordinal.sup_eq_bsup' {ι : Type u_1} (r : ι → ι → Prop) [ r] (f : ι → ordinal) :
theorem ordinal.bsup_eq_bsup {ι : Type u} (r r' : ι → ι → Prop) [ r] [ r'] (f : ι → ordinal) :
theorem ordinal.sup_eq_bsup {ι : Type u_1} (f : ι → ordinal) :
theorem ordinal.is_normal.bsup {f : ordinalordinal} (H : ordinal.is_normal f) {o : ordinal} (g : Π (a : ordinal), a < oordinal) (h : o 0) :
f (o.bsup g) = o.bsup (λ (a : ordinal) (h : a < o), f (g a h))
theorem ordinal.lt_bsup_of_ne_bsup {o : ordinal} {f : Π (a : ordinal), a < oordinal} :
(∀ (i : ordinal) (h : i < o), f i h o.bsup f) ∀ (i : ordinal) (h : i < o), f i h < o.bsup f
theorem ordinal.bsup_not_succ_of_ne_bsup {o : ordinal} {f : Π (a : ordinal), a < oordinal} (hf : ∀ {i : ordinal} (h : i < o), f i h o.bsup f) (a : ordinal) :
a < o.bsup fa.succ < o.bsup f
@[simp]
theorem ordinal.bsup_eq_zero_iff {o : ordinal} {f : Π (a : ordinal), a < oordinal} :
o.bsup f = 0 ∀ (i : ordinal) (hi : i < o), f i hi = 0
theorem ordinal.lt_bsup_of_limit {o : ordinal} {f : Π (a : ordinal), a < oordinal} (hf : ∀ {a a' : ordinal} (ha : a < o) (ha' : a' < o), a < a'f a ha < f a' ha') (ho : o.is_limit) (i : ordinal) (h : i < o) :
f i h < o.bsup f
theorem ordinal.bsup_id {o : ordinal} (ho : o.is_limit) :
o.bsup (λ (x : ordinal) (_x : x < o), x) = o
theorem ordinal.is_normal.bsup_eq {f : ordinalordinal} (H : ordinal.is_normal f) {o : ordinal} (h : o.is_limit) :
o.bsup (λ (x : ordinal) (_x : x < o), f x) = f o
noncomputable def ordinal.lsub {ι : Type u_1} (f : ι → ordinal) :

The least strict upper bound of a family of ordinals.

Equations
theorem ordinal.lsub_le {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
∀ (i : ι), f i < a
theorem ordinal.lt_lsub {ι : Type u_1} (f : ι → ordinal) (i : ι) :
f i <
theorem ordinal.sup_le_lsub {ι : Type u_1} (f : ι → ordinal) :
theorem ordinal.lsub_le_sup_succ {ι : Type u_1} (f : ι → ordinal) :
theorem ordinal.sup_succ_le_lsub {ι : Type u_1} (f : ι → ordinal) :
(ordinal.sup f).succ ∃ (i : ι), f i =
theorem ordinal.sup_succ_eq_lsub {ι : Type u_1} (f : ι → ordinal) :
(ordinal.sup f).succ = ∃ (i : ι), f i =
theorem ordinal.sup_eq_lsub_iff_succ {ι : Type u_1} (f : ι → ordinal) :
∀ (a : ordinal),
theorem ordinal.sup_eq_lsub_iff_lt_sup {ι : Type u_1} (f : ι → ordinal) :
∀ (i : ι), f i <
theorem ordinal.lsub_eq_zero {ι : Type u_1} [h : is_empty ι] (f : ι → ordinal) :
theorem ordinal.lsub_pos {ι : Type u_1} [h : nonempty ι] (f : ι → ordinal) :
@[simp]
theorem ordinal.lsub_eq_zero_iff {ι : Type u_1} {f : ι → ordinal} :
noncomputable def ordinal.blsub (o : ordinal) (f : Π (a : ordinal), a < oordinal) :

The bounded least strict upper bound of a family of ordinals.

Equations
theorem ordinal.blsub_eq_lsub' {ι : Type u_1} (r : ι → ι → Prop) [ r] {o : ordinal} (ho : = o) (f : Π (a : ordinal), a < oordinal) :
o.blsub f =
theorem ordinal.lsub_eq_lsub {ι : Type u} (r r' : ι → ι → Prop) [ r] [ r'] {o : ordinal} (ho : = o) (ho' : = o) (f : Π (a : ordinal), a < oordinal) :
= ordinal.lsub ho' f)
theorem ordinal.blsub_eq_lsub {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
o.blsub f =
theorem ordinal.lsub_eq_blsub' {ι : Type u_1} (r : ι → ι → Prop) [ r] (f : ι → ordinal) :
theorem ordinal.blsub_eq_blsub {ι : Type u} (r r' : ι → ι → Prop) [ r] [ r'] (f : ι → ordinal) :
theorem ordinal.lsub_eq_blsub {ι : Type u_1} (f : ι → ordinal) :
theorem ordinal.blsub_le {o : ordinal} {f : Π (a : ordinal), a < oordinal} {a : ordinal} :
o.blsub f a ∀ (i : ordinal) (h : i < o), f i h < a
theorem ordinal.lt_blsub {o : ordinal} (f : Π (a : ordinal), a < oordinal) (i : ordinal) (h : i < o) :
f i h < o.blsub f
theorem ordinal.bsup_le_blsub {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
o.bsup f o.blsub f
theorem ordinal.blsub_le_bsup_succ {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
o.blsub f (o.bsup f).succ
theorem ordinal.bsup_succ_le_blsub {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
(o.bsup f).succ o.blsub f ∃ (i : ordinal) (hi : i < o), f i hi = o.bsup f
theorem ordinal.bsup_succ_eq_blsub {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
(o.bsup f).succ = o.blsub f ∃ (i : ordinal) (hi : i < o), f i hi = o.bsup f
theorem ordinal.bsup_eq_blsub_iff_succ {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
o.bsup f = o.blsub f ∀ (a : ordinal), a < o.blsub fa.succ < o.blsub f
theorem ordinal.bsup_eq_blsub_iff_lt_bsup {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
o.bsup f = o.blsub f ∀ (i : ordinal) (hi : i < o), f i hi < o.bsup f
@[simp]
theorem ordinal.blsub_eq_zero_iff {o : ordinal} {f : Π (a : ordinal), a < oordinal} :
o.blsub f = 0 o = 0
theorem ordinal.blsub_eq_zero {o : ordinal} (ho : o = 0) (f : Π (a : ordinal), a < oordinal) :
o.blsub f = 0
theorem ordinal.blsub_pos {o : ordinal} (ho : 0 < o) (f : Π (a : ordinal), a < oordinal) :
0 < o.blsub f
theorem ordinal.blsub_type {α : Type u_1} (r : α → α → Prop) [ r] (f : Π (a : ordinal), ordinal) :
(ordinal.type r).blsub f = ordinal.lsub (λ (a : α), f a) _)
theorem ordinal.blsub_id {o : ordinal} :
o.blsub (λ (x : ordinal) (_x : x < o), x) = o

### Enumerating unbounded sets of ordinals with ordinals #

noncomputable def ordinal.enum_ord (S : set ordinal) (hS : S) :

Enumerator function for an unbounded set of ordinals.

Equations
theorem ordinal.enum_ord_def'_H {S : set ordinal} {hS : S} {o : ordinal} :
∃ (x : ordinal), x S o.blsub (λ (c : ordinal) (_x : c < o), hS c) x

The hypothesis that asserts that the `omin` from `enum_ord_def'` exists.

theorem ordinal.enum_ord_def' {S : set ordinal} (hS : S) (o : ordinal) :
hS o = ordinal.omin (S {b : ordinal | o.blsub (λ (c : ordinal) (_x : c < o), hS c) b}) ordinal.enum_ord_def'_H

The equation that characterizes `enum_ord` definitionally. This isn't the nicest expression to work with, so consider using `enum_ord_def` instead.

theorem ordinal.enum_ord_mem {S : set ordinal} (hS : S) (o : ordinal) :
hS o S
theorem ordinal.blsub_le_enum_ord {S : set ordinal} (hS : S) (o : ordinal) :
o.blsub (λ (c : ordinal) (_x : c < o), hS c) hS o
theorem ordinal.enum_ord_def_H {S : set ordinal} {hS : S} {o : ordinal} :
∃ (x : ordinal), x S ∀ (c : ordinal), c < o hS c < x

The hypothesis that asserts that the `omin` from `enum_ord_def` exists.

theorem ordinal.enum_ord_def {S : set ordinal} (hS : S) (o : ordinal) :
hS o = ordinal.omin (S {b : ordinal | ∀ (c : ordinal), c < o hS c < b}) ordinal.enum_ord_def_H

A more workable definition for `enum_ord`.

theorem ordinal.enum_ord.surjective {S : set ordinal} (hS : S) (s : ordinal) (H : s S) :
∃ (a : ordinal), hS a = s
noncomputable def ordinal.enum_ord.order_iso {S : set ordinal} (hS : S) :

An order isomorphism between an unbounded set of ordinals and the ordinals.

Equations
theorem ordinal.enum_ord_range {S : set ordinal} (hS : S) :
set.range hS) = S
theorem ordinal.eq_enum_ord {S : set ordinal} (hS : S) (f : ordinalordinal) :
= S f = hS

A characterization of `enum_ord`: it is the unique strict monotonic function with range `S`.

### Ordinal exponential #

noncomputable def ordinal.opow (a b : ordinal) :

The ordinal exponential, defined by transfinite recursion.

Equations
@[protected, instance]
noncomputable def ordinal.has_pow  :
Equations
theorem ordinal.zero_opow' (a : ordinal) :
0 ^ a = 1 - a
@[simp]
theorem ordinal.zero_opow {a : ordinal} (a0 : a 0) :
0 ^ a = 0
@[simp]
theorem ordinal.opow_zero (a : ordinal) :
a ^ 0 = 1
@[simp]
theorem ordinal.opow_succ (a b : ordinal) :
a ^ b.succ = (a ^ b) * a
theorem ordinal.opow_limit {a b : ordinal} (a0 : a 0) (h : b.is_limit) :
a ^ b = b.bsup (λ (c : ordinal) (_x : c < b), a ^ c)
theorem ordinal.opow_le_of_limit {a b c : ordinal} (a0 : a 0) (h : b.is_limit) :
a ^ b c ∀ (b' : ordinal), b' < ba ^ b' c
theorem ordinal.lt_opow_of_limit {a b c : ordinal} (b0 : b 0) (h : c.is_limit) :
a < b ^ c ∃ (c' : ordinal) (H : c' < c), a < b ^ c'
@[simp]
theorem ordinal.opow_one (a : ordinal) :
a ^ 1 = a
@[simp]
theorem ordinal.one_opow (a : ordinal) :
1 ^ a = 1
theorem ordinal.opow_pos {a : ordinal} (b : ordinal) (a0 : 0 < a) :
0 < a ^ b
theorem ordinal.opow_ne_zero {a : ordinal} (b : ordinal) (a0 : a 0) :
a ^ b 0
theorem ordinal.opow_is_normal {a : ordinal} (h : 1 < a) :
ordinal.is_normal (λ (_y : ordinal), a ^ _y)
theorem ordinal.opow_lt_opow_iff_right {a b c : ordinal} (a1 : 1 < a) :
a ^ b < a ^ c b < c
theorem ordinal.opow_le_opow_iff_right {a b c : ordinal} (a1 : 1 < a) :
a ^ b a ^ c b c
theorem ordinal.opow_right_inj {a b c : ordinal} (a1 : 1 < a) :
a ^ b = a ^ c b = c
theorem ordinal.opow_is_limit {a b : ordinal} (a1 : 1 < a) :
b.is_limit(a ^ b).is_limit
theorem ordinal.opow_is_limit_left {a b : ordinal} (l : a.is_limit) (hb : b 0) :
(a ^ b).is_limit
theorem ordinal.opow_le_opow_right {a b c : ordinal} (h₁ : 0 < a) (h₂ : b c) :
a ^ b a ^ c
theorem ordinal.opow_le_opow_left {a b : ordinal} (c : ordinal) (ab : a b) :
a ^ c b ^ c
theorem ordinal.le_opow_self {a : ordinal} (b : ordinal) (a1 : 1 < a) :
b a ^ b
theorem ordinal.opow_lt_opow_left_of_succ {a b c : ordinal} (ab : a < b) :
a ^ c.succ < b ^ c.succ
theorem ordinal.opow_add (a b c : ordinal) :
a ^ (b + c) = (a ^ b) * a ^ c
theorem ordinal.opow_dvd_opow (a : ordinal) {b c : ordinal} (h : b c) :
a ^ b a ^ c
theorem ordinal.opow_dvd_opow_iff {a b c : ordinal} (a1 : 1 < a) :
a ^ b a ^ c b c
theorem ordinal.opow_mul (a b c : ordinal) :
a ^ b * c = (a ^ b) ^ c

### Ordinal logarithm #

noncomputable def ordinal.log (b x : ordinal) :

The ordinal logarithm is the solution `u` to the equation `x = b ^ u * v + w` where `v < b` and `w < b ^ u`.

Equations
@[simp]
theorem ordinal.log_not_one_lt {b : ordinal} (b1 : ¬1 < b) (x : ordinal) :
b.log x = 0
theorem ordinal.log_def {b : ordinal} (b1 : 1 < b) (x : ordinal) :
b.log x = (ordinal.omin {o : ordinal | x < b ^ o} _).pred
@[simp]
theorem ordinal.log_zero (b : ordinal) :
b.log 0 = 0
theorem ordinal.succ_log_def {b x : ordinal} (b1 : 1 < b) (x0 : 0 < x) :
(b.log x).succ = ordinal.omin {o : ordinal | x < b ^ o} _
theorem ordinal.lt_opow_succ_log {b : ordinal} (b1 : 1 < b) (x : ordinal) :
x < b ^ (b.log x).succ
theorem ordinal.opow_log_le (b : ordinal) {x : ordinal} (x0 : 0 < x) :
b ^ b.log x x
theorem ordinal.le_log {b x c : ordinal} (b1 : 1 < b) (x0 : 0 < x) :
c b.log x b ^ c x
theorem ordinal.log_lt {b x c : ordinal} (b1 : 1 < b) (x0 : 0 < x) :
b.log x < c x < b ^ c
theorem ordinal.log_le_log (b : ordinal) {x y : ordinal} (xy : x y) :
b.log x b.log y
theorem ordinal.log_le_self (b x : ordinal) :
b.log x x
@[simp]
theorem ordinal.log_one (b : ordinal) :
b.log 1 = 0
theorem ordinal.opow_mul_add_pos {b v : ordinal} (hb : 0 < b) (u : ordinal) (hv : 0 < v) (w : ordinal) :
0 < (b ^ u) * v + w
theorem ordinal.opow_mul_add_lt_opow_mul_succ {b u w : ordinal} (v : ordinal) (hw : w < b ^ u) :
(b ^ u) * v + w < (b ^ u) * v.succ
theorem ordinal.opow_mul_add_lt_opow_succ {b u v w : ordinal} (hvb : v < b) (hw : w < b ^ u) :
(b ^ u) * v + w < b ^ u.succ
theorem ordinal.log_opow_mul_add {b u v w : ordinal} (hb : 1 < b) (hv : 0 < v) (hvb : v < b) (hw : w < b ^ u) :
b.log ((b ^ u) * v + w) = u
@[simp]
theorem ordinal.log_opow {b : ordinal} (hb : 1 < b) (x : ordinal) :
b.log (b ^ x) = x
theorem ordinal.add_log_le_log_mul {x y : ordinal} (b : ordinal) (x0 : 0 < x) (y0 : 0 < y) :
b.log x + b.log y b.log (x * y)

### The Cantor normal form #

theorem ordinal.CNF_aux {b o : ordinal} (b0 : b 0) (o0 : o 0) :
o % b ^ b.log o < o
noncomputable def ordinal.CNF_rec {b : ordinal} (b0 : b 0) {C : ordinalSort u_2} (H0 : C 0) (H : Π (o : ordinal), o 0o % b ^ b.log o < oC (o % b ^ b.log o)C o) (o : ordinal) :
C o

Proving properties of ordinals by induction over their Cantor normal form.

Equations
@[simp]
theorem ordinal.CNF_rec_zero {b : ordinal} (b0 : b 0) {C : ordinalSort u_2} {H0 : C 0} {H : Π (o : ordinal), o 0o % b ^ b.log o < oC (o % b ^ b.log o)C o} :
H0 H 0 = H0
@[simp]
theorem ordinal.CNF_rec_ne_zero {b : ordinal} (b0 : b 0) {C : ordinalSort u_2} {H0 : C 0} {H : Π (o : ordinal), o 0o % b ^ b.log o < oC (o % b ^ b.log o)C o} {o : ordinal} (o0 : o 0) :
H0 H o = H o o0 _ H0 H (o % b ^ b.log o))
noncomputable def ordinal.CNF (b : ordinal := ω) (o : ordinal) :

The Cantor normal form of an ordinal is the list of coefficients in the base-`b` expansion of `o`.

CNF b (b ^ u₁ * v₁ + b ^ u₂ * v₂) = [(u₁, v₁), (u₂, v₂)]

Equations
@[simp]
theorem ordinal.zero_CNF (o : ordinal) :
@[simp]
theorem ordinal.CNF_zero (b : ordinal := ω) :
theorem ordinal.CNF_ne_zero {b o : ordinal} (b0 : b 0) (o0 : o 0) :
o = (b.log o, o / b ^ b.log o) :: (o % b ^ b.log o)
theorem ordinal.one_CNF {o : ordinal} (o0 : o 0) :
o = [(0, o)]
theorem ordinal.CNF_foldr {b : ordinal} (b0 : b 0) (o : ordinal) :
list.foldr (λ (p : (r : ordinal), (b ^ p.fst) * p.snd + r) 0 o) = o
theorem ordinal.CNF_pairwise_aux (b : ordinal := ω) (o : ordinal) :
(∀ (p : , p op.fst o) list.pairwise (λ (p q : , q.fst < p.fst) o)
theorem ordinal.CNF_pairwise (b : ordinal := ω) (o : ordinal) :
list.pairwise (λ (p q : , q.fst < p.fst) o)
theorem ordinal.CNF_fst_le_log (b : ordinal := ω) (o : ordinal) (p : ordinal × ordinal) (H : p o) :
p.fst o
theorem ordinal.CNF_fst_le (b : ordinal := ω) (o : ordinal) (p : ordinal × ordinal) (H : p o) :
p.fst o
theorem ordinal.CNF_snd_lt {b : ordinal} (b1 : 1 < b) (o : ordinal) (p : ordinal × ordinal) (H : p o) :
p.snd < b
theorem ordinal.CNF_sorted (b : ordinal := ω) (o : ordinal) :
o))

### Casting naturals into ordinals, compatibility with operations #

@[simp]
theorem ordinal.nat_cast_mul {m n : } :
m * n = (m) * n
@[simp]
theorem ordinal.nat_cast_opow {m n : } :
(m ^ n) = m ^ n
@[simp]
theorem ordinal.nat_cast_le {m n : } :
m n m n
@[simp]
theorem ordinal.nat_cast_lt {m n : } :
m < n m < n
@[simp]
theorem ordinal.nat_cast_inj {m n : } :
m = n m = n
@[simp]
theorem ordinal.nat_cast_eq_zero {n : } :
n = 0 n = 0
theorem ordinal.nat_cast_ne_zero {n : } :
n 0 n 0
@[simp]
theorem ordinal.nat_cast_pos {n : } :
0 < n 0 < n
@[simp]
theorem ordinal.nat_cast_sub {m n : } :
(m - n) = m - n
@[simp]
theorem ordinal.nat_cast_div {m n : } :
(m / n) = m / n
@[simp]
theorem ordinal.nat_cast_mod {m n : } :
(m % n) = m % n
@[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_fin (n : ) :
@[simp]
theorem ordinal.lift_nat_cast (n : ) :
theorem ordinal.lift_type_fin (n : ) :
theorem ordinal.type_fintype {α : Type u_1} (r : α → α → Prop) [ r] [fintype α] :

### Properties of `omega`#

@[simp]
theorem cardinal.ord_omega  :
@[simp]
theorem cardinal.add_one_of_omega_le {c : cardinal} (h : ω c) :
c + 1 = c
theorem ordinal.lt_omega {o : ordinal} :
o < ω ∃ (n : ), o = n
theorem ordinal.nat_lt_omega (n : ) :
theorem ordinal.omega_pos  :
0 < ω
theorem ordinal.omega_le {o : ordinal} :
ω o ∀ (n : ), n o
theorem ordinal.nat_lt_limit {o : ordinal} (h : o.is_limit) (n : ) :
n < o
theorem ordinal.add_omega {a : ordinal} (h : a < ω) :
a + ω = ω
theorem ordinal.add_lt_omega {a b : ordinal} (ha : a < ω) (hb : b < ω) :
a + b < ω
theorem ordinal.mul_lt_omega {a b : ordinal} (ha : a < ω) (hb : b < ω) :
a * b < ω
theorem ordinal.opow_lt_omega {a b : ordinal} (ha : a < ω) (hb : b < ω) :
a ^ b < ω
theorem ordinal.add_omega_opow {a b : ordinal} (h : a < ω ^ b) :
a + ω ^ b = ω ^ b
theorem ordinal.add_lt_omega_opow {a b c : ordinal} (h₁ : a < ω ^ c) (h₂ : b < ω ^ c) :
a + b < ω ^ c
theorem ordinal.add_absorp {a b c : ordinal} (h₁ : a < ω ^ b) (h₂ : ω ^ b c) :
a + c = c
theorem ordinal.add_absorp_iff {o : ordinal} (o0 : 0 < o) :
(∀ (a : ordinal), a < oa + o = o) ∃ (a : ordinal), o = ω ^ a
theorem ordinal.add_mul_limit_aux {a b c : ordinal} (ba : b + a = a) (l : c.is_limit) (IH : ∀ (c' : ordinal), c' < c(a + b) * c'.succ = a * c'.succ + b) :
(a + b) * c = a * c
theorem ordinal.add_mul_succ {a b : ordinal} (c : ordinal) (ba : b + a = a) :
(a + b) * c.succ = a * c.succ + b
theorem ordinal.add_mul_limit {a b c : ordinal} (ba : b + a = a) (l : c.is_limit) :
(a + b) * c = a * c
theorem ordinal.mul_omega {a : ordinal} (a0 : 0 < a) (ha : a < ω) :
a * ω = ω
theorem ordinal.mul_lt_omega_opow {a b c : ordinal} (c0 : 0 < c) (ha : a < ω ^ c) (hb : b < ω) :
a * b < ω ^ c
theorem ordinal.mul_omega_dvd {a : ordinal} (a0 : 0 < a) (ha : a < ω) {b : ordinal} :
ω ba * b = b
theorem ordinal.mul_omega_opow_opow {a b : ordinal} (a0 : 0 < a) (h : a < ω ^ ω ^ b) :
a * ω ^ ω ^ b = ω ^ ω ^ b
theorem ordinal.opow_omega {a : ordinal} (a1 : 1 < a) (h : a < ω) :
a ^ ω = ω

### Fixed points of normal functions #

noncomputable def ordinal.nfp (f : ordinalordinal) (a : ordinal) :

The next fixed point function, the least fixed point of the normal function `f` above `a`.

Equations
theorem ordinal.iterate_le_nfp (f : ordinalordinal) (a : ordinal) (n : ) :
f^[n] a a
theorem ordinal.le_nfp_self (f : ordinalordinal) (a : ordinal) :
a a
theorem ordinal.is_normal.lt_nfp {f : ordinalordinal} (H : ordinal.is_normal f) {a b : ordinal} :
f b < a b < a
theorem ordinal.is_normal.nfp_le {f : ordinalordinal} (H : ordinal.is_normal f) {a b : ordinal} :
a f b a b
theorem ordinal.is_normal.nfp_le_fp {f : ordinalordinal} (H : ordinal.is_normal f) {a b : ordinal} (ab : a b) (h : f b b) :
a b
theorem ordinal.is_normal.nfp_fp {f : ordinalordinal} (H : ordinal.is_normal f) (a : ordinal) :
f a) = a
theorem ordinal.is_normal.le_nfp {f : ordinalordinal} (H : ordinal.is_normal f) {a b : ordinal} :
f b a b a
theorem ordinal.nfp_eq_self {f : ordinalordinal} {a : ordinal} (h : f a = a) :
a = a
noncomputable def ordinal.deriv (f : ordinalordinal) (o : ordinal) :

The derivative of a normal function `f` is the sequence of fixed points of `f`.

Equations
@[simp]
theorem ordinal.deriv_zero (f : ordinalordinal) :
= 0
@[simp]
theorem ordinal.deriv_succ (f : ordinalordinal) (o : ordinal) :
= o).succ
theorem ordinal.deriv_limit (f : ordinalordinal) {o : ordinal} :
o.is_limit = o.bsup (λ (a : ordinal) (_x : a < o), a)
theorem ordinal.is_normal.deriv_fp {f : ordinalordinal} (H : ordinal.is_normal f) (o : ordinal) :
f o) =
theorem ordinal.is_normal.fp_iff_deriv {f : ordinalordinal} (H : ordinal.is_normal f) {a : ordinal} :
f a a ∃ (o : ordinal), a =