mathlib documentation

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 #

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

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

Various other basic arithmetic results are given in principal.lean instead.

Further properties of addition on ordinals #

@[simp]
theorem ordinal.lift_add (a b : ordinal) :
(a + b).lift = a.lift + b.lift
@[simp]
theorem ordinal.add_succ (o₁ o₂ : ordinal) :
o₁ + order.succ o₂ = order.succ (o₁ + o₂)
@[simp]
theorem ordinal.succ_zero  :
@[simp]
theorem ordinal.succ_one  :
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) :
@[simp]
theorem ordinal.card_succ (o : ordinal) :
theorem ordinal.add_left_cancel (a : ordinal) {b c : ordinal} :
a + b = a + c b = c
theorem ordinal.lt_one_iff_zero {a : ordinal} :
a < 1 a = 0
theorem ordinal.add_le_add_iff_right {a b : ordinal} (n : ) :
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
@[protected]
theorem ordinal.one_ne_zero  :
1 0
@[protected, instance]
@[simp]
theorem ordinal.zero_lt_one  :
0 < 1
@[protected, instance]
Equations
@[protected, instance]
noncomputable def ordinal.unique_out_one  :
Equations
theorem ordinal.le_one_iff {a : ordinal} :
a 1 a = 0 a = 1
theorem ordinal.add_eq_zero_iff {a b : ordinal} :
a + b = 0 a = 0 b = 0
theorem ordinal.left_eq_zero_of_add_eq_zero {a b : ordinal} (h : a + b = 0) :
a = 0
theorem ordinal.right_eq_zero_of_add_eq_zero {a b : ordinal} (h : a + b = 0) :
b = 0

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) :
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 = order.succ a
theorem ordinal.pred_lt_iff_is_succ {o : ordinal} :
o.pred < o ∃ (a : ordinal), o = order.succ a
theorem ordinal.succ_lt_of_not_succ {o b : ordinal} (h : ¬∃ (a : ordinal), o = order.succ a) :
order.succ b < o b < o
theorem ordinal.lt_pred {a b : ordinal} :
theorem ordinal.pred_le {a b : ordinal} :
@[simp]
theorem ordinal.lift_is_succ {o : ordinal} :
(∃ (a : ordinal), o.lift = order.succ a) ∃ (a : ordinal), o = order.succ a
@[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 = order.succ a
theorem ordinal.succ_lt_of_is_limit {o a : ordinal} (h : o.is_limit) :
order.succ a < o a < o
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
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 = order.succ a) o.is_limit
noncomputable def ordinal.limit_rec_on {C : ordinalSort u_2} (o : ordinal) (H₁ : C 0) (H₂ : Π (o : ordinal), C oC (order.succ o)) (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 (order.succ o)) (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 (order.succ o)) (H₃ : Π (o : ordinal), o.is_limit(Π (o' : ordinal), o' < oC o')C o) :
(order.succ o).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 (order.succ o)) (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₃)
@[protected, instance]
Equations
theorem ordinal.has_succ_of_type_succ_lt {α : Type u_1} {r : α → α → Prop} [wo : is_well_order α r] (h : ∀ (a : ordinal), a < ordinal.type rorder.succ a < ordinal.type r) (x : α) :
∃ (y : α), r x y
theorem ordinal.out_no_max_of_succ_lt {o : ordinal} (ho : ∀ (a : ordinal), a < oorder.succ a < o) :
theorem ordinal.bounded_singleton {α : Type u_1} {r : α → α → Prop} [is_well_order α r] (hr : (ordinal.type r).is_limit) (x : α) :

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_iff_strict_mono_limit (f : ordinalordinal) :
ordinal.is_normal f strict_mono f ∀ (o : ordinal), o.is_limit∀ (a : ordinal), (∀ (b : ordinal), b < of b a)f o a
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.self_le {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 : set ordinal) (p0 : p.nonempty) (b : ordinal) (H₂ : ∀ (o : ordinal), b o ∀ (a : ordinal), a pa o) {o : ordinal} :
f b o ∀ (a : ordinal), a pf a o
theorem ordinal.is_normal.le_set' {α : Type u_1} {f : ordinalordinal} (H : ordinal.is_normal f) (p : set α) (g : α → ordinal) (p0 : p.nonempty) (b : ordinal) (H₂ : ∀ (o : ordinal), b o ∀ (a : α), a pg a o) {o : ordinal} :
f b o ∀ (a : α), a pf (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.is_normal.le_iff_eq {f : ordinalordinal} (H : ordinal.is_normal f) {a : ordinal} :
f a a f a = a
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 #

theorem ordinal.sub_nonempty {a b : ordinal} :
{o : ordinal | a b + o}.nonempty

The set in the definition of subtraction is nonempty.

@[protected, instance]
noncomputable def ordinal.has_sub  :

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

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)
theorem ordinal.add_sub_add_cancel (a b c : ordinal) :
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]
theorem ordinal.one_add_of_omega_le {o : ordinal} (h : ordinal.omega 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) [is_well_order α r] [is_well_order β s] :
@[protected, instance]
Equations
@[protected, instance]
@[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
@[protected, instance]
Equations
theorem ordinal.mul_succ (a b : ordinal) :
a * order.succ b = a * b + a
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_of_limit {a b c : ordinal} (h : b.is_limit) :
a * b c ∀ (b' : ordinal), b' < ba * b' c
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
theorem ordinal.smul_eq_mul (n : ) (a : ordinal) :
n a = a * n

Division on ordinals #

theorem ordinal.div_nonempty {a b : ordinal} (h : b 0) :
{o : ordinal | a < b * order.succ o}.nonempty

The set in the definition of division is nonempty.

@[protected, instance]
noncomputable def ordinal.has_div  :

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

Equations
@[simp]
theorem ordinal.div_zero (a : ordinal) :
a / 0 = 0
theorem ordinal.div_def (a : ordinal) {b : ordinal} (h : b 0) :
a / b = has_Inf.Inf {o : ordinal | a < b * order.succ o}
theorem ordinal.lt_mul_succ_div (a : ordinal) {b : ordinal} (h : b 0) :
a < b * order.succ (a / b)
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 * order.succ c
theorem ordinal.lt_div {a b c : ordinal} (c0 : c 0) :
a < b / c c * order.succ a 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.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) [is_well_order ι r] (f : ι → α) (a : ordinal) (H : a < ordinal.type r) :
α

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), a < ordinal.type well_ordering_rel → α

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) [is_well_order ι r] {o : ordinal} (ho : ordinal.type r = 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
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) [is_well_order ι r] (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) [is_well_order ι r] {o : ordinal} (ho : ordinal.type r = o) (f : Π (a : ordinal), a < o → α) (i : ordinal) (hi : i < o) :
@[simp]
theorem ordinal.family_of_bfamily_enum {α : Type u_1} (o : ordinal) (f : Π (a : ordinal), a < o → α) (i : ordinal) (hi : i < o) :
def ordinal.brange {α : Type u_1} (o : ordinal) (f : Π (a : ordinal), a < o → α) :
set α

The range of a family indexed by ordinals.

Equations
theorem ordinal.mem_brange {α : Type u_1} {o : ordinal} {f : Π (a : ordinal), a < o → α} {a : α} :
a o.brange f ∃ (i : ordinal) (hi : i < o), f i hi = a
theorem ordinal.mem_brange_self {α : Type u_1} {o : ordinal} (f : Π (a : ordinal), a < o → α) (i : ordinal) (hi : i < o) :
f i hi o.brange f
@[simp]
theorem ordinal.range_family_of_bfamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [is_well_order ι r] {o : ordinal} (ho : ordinal.type r = o) (f : Π (a : ordinal), a < o → α) :
@[simp]
theorem ordinal.range_family_of_bfamily {α : Type u_1} {o : ordinal} (f : Π (a : ordinal), a < o → α) :
@[simp]
theorem ordinal.brange_bfamily_of_family' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [is_well_order ι r] (f : ι → α) :
@[simp]
theorem ordinal.brange_bfamily_of_family {α : Type u_1} {ι : Type u} (f : ι → α) :
@[simp]
theorem ordinal.brange_const {α : Type u_1} {o : ordinal} (ho : o 0) {c : α} :
o.brange (λ (_x : ordinal) (_x : _x < o), c) = {c}
theorem ordinal.comp_bfamily_of_family' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [is_well_order ι r] (f : ι → α) (g : α → β) :
theorem ordinal.comp_bfamily_of_family {α : Type u_1} {β : Type u_2} {ι : Type u} (f : ι → α) (g : α → β) :
theorem ordinal.comp_family_of_bfamily' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [is_well_order ι r] {o : ordinal} (ho : ordinal.type r = o) (f : Π (a : ordinal), a < o → α) (g : α → β) :
g ordinal.family_of_bfamily' r ho f = ordinal.family_of_bfamily' r ho (λ (i : ordinal) (hi : i < o), g (f i hi))
theorem ordinal.comp_family_of_bfamily {α : Type u_1} {β : Type u_2} {o : ordinal} (f : Π (a : ordinal), a < o → α) (g : α → β) :
g o.family_of_bfamily f = o.family_of_bfamily (λ (i : ordinal) (hi : i < o), g (f i hi))

Supremum of a family of ordinals #

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

The supremum of a family of ordinals

Equations
@[simp]
theorem ordinal.Sup_eq_sup {ι : Type u} (f : ι → ordinal) :
theorem ordinal.bdd_above_range {ι : Type u} (f : ι → ordinal) :

The range of an indexed ordinal function, whose outputs live in a higher universe than the inputs, is always bounded above. See ordinal.lsub for an explicit bound.

theorem ordinal.le_sup {ι : Type u_1} (f : ι → ordinal) (i : ι) :
theorem ordinal.sup_le_iff {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
ordinal.sup f a ∀ (i : ι), f i a
theorem ordinal.sup_le {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
(∀ (i : ι), f i a)ordinal.sup f a
theorem ordinal.lt_sup {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
a < ordinal.sup f ∃ (i : ι), a < f i
theorem ordinal.ne_sup_iff_lt_sup {ι : Type u_1} {f : ι → ordinal} :
(∀ (i : ι), f i ordinal.sup f) ∀ (i : ι), f i < ordinal.sup f
theorem ordinal.sup_not_succ_of_ne_sup {ι : Type u_1} {f : ι → ordinal} (hf : ∀ (i : ι), f i ordinal.sup f) {a : ordinal} (hao : a < ordinal.sup f) :
@[simp]
theorem ordinal.sup_eq_zero_iff {ι : Type u_1} {f : ι → ordinal} :
ordinal.sup f = 0 ∀ (i : ι), f i = 0
theorem ordinal.is_normal.sup {f : ordinalordinal} (H : ordinal.is_normal f) {ι : Type u_1} (g : ι → ordinal) (h : nonempty ι) :
@[simp]
theorem ordinal.sup_empty {ι : Type u_1} [is_empty ι] (f : ι → ordinal) :
@[simp]
theorem ordinal.sup_const {ι : Type u_1} [hι : nonempty ι] (o : ordinal) :
ordinal.sup (λ (_x : ι), o) = o
@[simp]
theorem ordinal.sup_unique {ι : Type u_1} [unique ι] (f : ι → ordinal) :
theorem ordinal.sup_le_of_range_subset {ι : Type u} {ι' : Type v} {f : ι → ordinal} {g : ι' → ordinal} (h : set.range f set.range g) :
theorem ordinal.sup_eq_of_range_eq {ι : Type u} {ι' : Type v} {f : ι → ordinal} {g : ι' → ordinal} (h : set.range f = set.range g) :
theorem ordinal.unbounded_range_of_sup_ge {α β : Type u} (r : α → α → Prop) [is_well_order α r] (f : β → α) (h : ordinal.type r ordinal.sup (ordinal.typein r f)) :
theorem ordinal.le_sup_shrink_equiv {s : set ordinal} (hs : small s) (a : ordinal) (ha : a s) :
theorem ordinal.supr_ord {ι : Sort u_1} {f : ι → cardinal} (hf : bdd_above (set.range f)) :
(supr f).ord = ⨆ (i : ι), (f i).ord
theorem ordinal.sup_eq_sup {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [is_well_order ι r] [is_well_order ι' r'] {o : ordinal} (ho : ordinal.type r = o) (ho' : ordinal.type r' = o) (f : Π (a : ordinal), a < oordinal) :
noncomputable def ordinal.bsup (o : ordinal) (f : Π (a : ordinal), a < oordinal) :

The supremum of a family of ordinals indexed by the set of ordinals less than some o : ordinal.{u}. This is a special case of sup over the family provided by family_of_bfamily.

Equations
@[simp]
theorem ordinal.sup_eq_bsup {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
@[simp]
theorem ordinal.sup_eq_bsup' {o : ordinal} {ι : Type u_1} (r : ι → ι → Prop) [is_well_order ι r] (ho : ordinal.type r = o) (f : Π (a : ordinal), a < oordinal) :
@[simp]
theorem ordinal.Sup_eq_bsup {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
@[simp]
theorem ordinal.bsup_eq_sup' {ι : Type u_1} (r : ι → ι → Prop) [is_well_order ι r] (f : ι → ordinal) :
theorem ordinal.bsup_eq_bsup {ι : Type u} (r r' : ι → ι → Prop) [is_well_order ι r] [is_well_order ι r'] (f : ι → ordinal) :
theorem ordinal.bsup_congr {o₁ o₂ : ordinal} (f : Π (a : ordinal), a < o₁ordinal) (ho : o₁ = o₂) :
o₁.bsup f = o₂.bsup (λ (a : ordinal) (h : a < o₂), f a _)
theorem ordinal.bsup_le_iff {o : ordinal} {f : Π (a : ordinal), a < oordinal} {a : ordinal} :
o.bsup f a ∀ (i : ordinal) (h : i < o), f i h a
theorem ordinal.bsup_le {o : ordinal} {f : Π (b : ordinal), b < oordinal} {a : ordinal} :
(∀ (i : ordinal) (h : i < o), f i h a)o.bsup f 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.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 forder.succ a < 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 : ∀ (a : ordinal), a < oorder.succ a < o) (i : ordinal) (h : i < o) :
f i h < o.bsup f
theorem ordinal.bsup_succ_of_mono {o : ordinal} {f : Π (a : ordinal), a < order.succ oordinal} (hf : ∀ {i j : ordinal} (hi : i < order.succ o) (hj : j < order.succ o), i jf i hi f j hj) :
(order.succ o).bsup f = f o _
@[simp]
theorem ordinal.bsup_zero (f : Π (a : ordinal), a < 0ordinal) :
0.bsup f = 0
theorem ordinal.bsup_const {o : ordinal} (ho : o 0) (a : ordinal) :
o.bsup (λ (_x : ordinal) (_x : _x < o), a) = a
@[simp]
theorem ordinal.bsup_one (f : Π (a : ordinal), a < 1ordinal) :
theorem ordinal.bsup_le_of_brange_subset {o : ordinal} {o' : ordinal} {f : Π (a : ordinal), a < oordinal} {g : Π (a : ordinal), a < o'ordinal} (h : o.brange f o'.brange g) :
o.bsup f o'.bsup g
theorem ordinal.bsup_eq_of_brange_eq {o : ordinal} {o' : ordinal} {f : Π (a : ordinal), a < oordinal} {g : Π (a : ordinal), a < o'ordinal} (h : o.brange f = o'.brange g) :
o.bsup f = o'.bsup g
noncomputable def ordinal.lsub {ι : Type u_1} (f : ι → ordinal) :

The least strict upper bound of a family of ordinals.

Equations
@[simp]
theorem ordinal.sup_eq_lsub {ι : Type u_1} (f : ι → ordinal) :
theorem ordinal.lsub_le_iff {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
ordinal.lsub f a ∀ (i : ι), f i < a
theorem ordinal.lsub_le {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
(∀ (i : ι), f i < a)ordinal.lsub f a
theorem ordinal.lt_lsub {ι : Type u_1} (f : ι → ordinal) (i : ι) :
theorem ordinal.lt_lsub_iff {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
a < ordinal.lsub f ∃ (i : ι), a 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) :
theorem ordinal.sup_succ_eq_lsub {ι : Type u_1} (f : ι → ordinal) :
theorem ordinal.sup_eq_lsub_iff_succ {ι : Type u_1} (f : ι → ordinal) :
theorem ordinal.sup_eq_lsub_iff_lt_sup {ι : Type u_1} (f : ι → ordinal) :
ordinal.sup f = ordinal.lsub f ∀ (i : ι), f i < ordinal.sup f
@[simp]
theorem ordinal.lsub_empty {ι : 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} :
@[simp]
theorem ordinal.lsub_const {ι : Type u_1} [hι : nonempty ι] (o : ordinal) :
ordinal.lsub (λ (_x : ι), o) = order.succ o
@[simp]
theorem ordinal.lsub_unique {ι : Type u_1} [hι : unique ι] (f : ι → ordinal) :
theorem ordinal.lsub_le_of_range_subset {ι : Type u} {ι' : Type v} {f : ι → ordinal} {g : ι' → ordinal} (h : set.range f set.range g) :
theorem ordinal.lsub_eq_of_range_eq {ι : Type u} {ι' : Type v} {f : ι → ordinal} {g : ι' → ordinal} (h : set.range f = set.range g) :
theorem ordinal.lsub_not_mem_range {ι : Type u_1} (f : ι → ordinal) :
theorem ordinal.nonempty_compl_range {ι : Type u} (f : ι → ordinal) :
theorem ordinal.sup_typein_limit {o : ordinal} (ho : ∀ (a : ordinal), a < oorder.succ a < o) :
noncomputable def ordinal.blsub (o : ordinal) (f : Π (a : ordinal), a < oordinal) :

The least strict upper bound of a family of ordinals indexed by the set of ordinals less than some o : ordinal.{u}.

This is to lsub as bsup is to sup.

Equations
@[simp]
theorem ordinal.bsup_eq_blsub (o : ordinal) (f : Π (a : ordinal), a < oordinal) :
o.bsup (λ (a : ordinal) (ha : a < o), order.succ (f a ha)) = o.blsub f
theorem ordinal.lsub_eq_blsub' {ι : Type u_1} (r : ι → ι → Prop) [is_well_order ι r] {o : ordinal} (ho : ordinal.type r = o) (f : Π (a : ordinal), a < oordinal) :
theorem ordinal.lsub_eq_lsub {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [is_well_order ι r] [is_well_order ι' r'] {o : ordinal} (ho : ordinal.type r = o) (ho' : ordinal.type r' = o) (f : Π (a : ordinal), a < oordinal) :
@[simp]
theorem ordinal.lsub_eq_blsub {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
@[simp]
theorem ordinal.blsub_eq_lsub' {ι : Type u_1} (r : ι → ι → Prop) [is_well_order ι r] (f : ι → ordinal) :
theorem ordinal.blsub_eq_blsub {ι : Type u} (r r' : ι → ι → Prop) [is_well_order ι r] [is_well_order ι r'] (f : ι → ordinal) :
theorem ordinal.blsub_congr {o₁ o₂ : ordinal} (f : Π (a : ordinal), a < o₁ordinal) (ho : o₁ = o₂) :
o₁.blsub f = o₂.blsub (λ (a : ordinal) (h : a < o₂), f a _)
theorem ordinal.blsub_le_iff {o : ordinal} {f : Π (a : ordinal), a < oordinal} {a : ordinal} :
o.blsub f a ∀ (i : ordinal) (h : i < o), f i h < a
theorem ordinal.blsub_le {o : ordinal} {f : Π (b : ordinal), b < oordinal} {a : ordinal} :
(∀ (i : ordinal) (h : i < o), f i h < a)o.blsub f 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.lt_blsub_iff {o : ordinal} {f : Π (a : ordinal), a < oordinal} {a : ordinal} :
a < o.blsub f ∃ (i : ordinal) (hi : i < o), a f i hi
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) :
theorem ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
o.bsup f = o.blsub f order.succ (o.bsup f) = o.blsub f
theorem ordinal.bsup_succ_le_blsub {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
order.succ (o.bsup f) 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) :
order.succ (o.bsup f) = 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 forder.succ a < 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
theorem ordinal.bsup_eq_blsub_of_lt_succ_limit {o : ordinal} (ho : o.is_limit) {f : Π (a : ordinal), a < oordinal} (hf : ∀ (a : ordinal) (ha : a < o), f a ha < f (order.succ a) _) :
o.bsup f = o.blsub f
theorem ordinal.blsub_succ_of_mono {o : ordinal} {f : Π (a : ordinal), a < order.succ oordinal} (hf : ∀ {i j : ordinal} (hi : i < order.succ o) (hj : j < order.succ o), i jf i hi f j hj) :
@[simp]
theorem ordinal.blsub_eq_zero_iff {o : ordinal} {f : Π (a : ordinal), a < oordinal} :
o.blsub f = 0 o = 0
@[simp]
theorem ordinal.blsub_zero (f : Π (a : ordinal), a < 0ordinal) :
0.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) [is_well_order α r] (f : Π (a : ordinal), a < ordinal.type rordinal) :
(ordinal.type r).blsub f = ordinal.lsub (λ (a : α), f (ordinal.typein r a) _)
theorem ordinal.blsub_const {o : ordinal} (ho : o 0) (a : ordinal) :
o.blsub (λ (_x : ordinal) (_x : _x < o), a) = order.succ a
@[simp]
theorem ordinal.blsub_one (f : Π (a : ordinal), a < 1ordinal) :
@[simp]
theorem ordinal.blsub_id (o : ordinal) :
o.blsub (λ (x : ordinal) (_x : x < o), x) = o
theorem ordinal.bsup_id_limit {o : ordinal} :
(∀ (a : ordinal), a < oorder.succ a < o)o.bsup (λ (x : ordinal) (_x : x < o), x) = o
@[simp]
theorem ordinal.bsup_id_succ (o : ordinal) :
(order.succ o).bsup (λ (x : ordinal) (_x : x < order.succ o), x) = o
theorem ordinal.blsub_le_of_brange_subset {o : ordinal} {o' : ordinal} {f : Π (a : ordinal), a < oordinal} {g : Π (a : ordinal), a < o'ordinal} (h : o.brange f o'.brange g) :
o.blsub f o'.blsub g
theorem ordinal.blsub_eq_of_brange_eq {o : ordinal} {o' : ordinal} {f : Π (a : ordinal), a < oordinal} {g : Π (a : ordinal), a < o'ordinal} (h : {o_1 : ordinal | ∃ (i : ordinal) (hi : i < o), f i hi = o_1} = {o : ordinal | ∃ (i : ordinal) (hi : i < o'), g i hi = o}) :
o.blsub f = o'.blsub g
theorem ordinal.bsup_comp {o o' : ordinal} {f : Π (a : ordinal), a < oordinal} (hf : ∀ {i j : ordinal} (hi : i < o) (hj : j < o), i jf i hi f j hj) {g : Π (a : ordinal), a < o'ordinal} (hg : o'.blsub g = o) :
o'.bsup (λ (a : ordinal) (ha : a < o'), f (g a ha) _) = o.bsup f
theorem ordinal.blsub_comp {o o' : ordinal} {f : Π (a : ordinal), a < oordinal} (hf : ∀ {i j : ordinal} (hi : i < o) (hj : j < o), i jf i hi f j hj) {g : Π (a : ordinal), a < o'ordinal} (hg : o'.blsub g = o) :
o'.blsub (λ (a : ordinal) (ha : a < o'), f (g a ha) _) = o.blsub f
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
theorem ordinal.is_normal.blsub_eq {f : ordinalordinal} (H : ordinal.is_normal f) {o : ordinal} (h : o.is_limit) :
o.blsub (λ (x : ordinal) (_x : x < o), f x) = f o
theorem ordinal.is_normal_iff_lt_succ_and_bsup_eq {f : ordinalordinal} :
ordinal.is_normal f (∀ (a : ordinal), f a < f (order.succ a)) ∀ (o : ordinal), o.is_limito.bsup (λ (x : ordinal) (_x : x < o), f x) = f o
theorem ordinal.is_normal_iff_lt_succ_and_blsub_eq {f : ordinalordinal} :
ordinal.is_normal f (∀ (a : ordinal), f a < f (order.succ a)) ∀ (o : ordinal), o.is_limito.blsub (λ (x : ordinal) (_x : x < o), f x) = f o
theorem ordinal.is_normal.eq_iff_zero_and_succ {f g : ordinalordinal} (hf : ordinal.is_normal f) (hg : ordinal.is_normal g) :
f = g f 0 = g 0 ∀ (a : ordinal), f a = g af (order.succ a) = g (order.succ a)

Minimum excluded ordinals #

noncomputable def ordinal.mex {ι : Type u} (f : ι → ordinal) :

The minimum excluded ordinal in a family of ordinals.

Equations
theorem ordinal.mex_not_mem_range {ι : Type u} (f : ι → ordinal) :
theorem ordinal.ne_mex {ι : Type u_1} (f : ι → ordinal) (i : ι) :
theorem ordinal.mex_le_of_ne {ι : Type u_1} {f : ι → ordinal} {a : ordinal} (ha : ∀ (i : ι), f i a) :
theorem ordinal.exists_of_lt_mex {ι : Type u_1} {f : ι → ordinal} {a : ordinal} (ha : a < ordinal.mex f) :
∃ (i : ι), f i = a
theorem ordinal.mex_le_lsub {ι : Type u_1} (f : ι → ordinal) :
theorem ordinal.mex_monotone {α β : Type u_1} {f : α → ordinal} {g : β → ordinal} (h : set.range f set.range g) :
theorem ordinal.mex_lt_ord_succ_mk {ι : Type (max u_1 u_2)} (f : ι → ordinal) :
noncomputable def ordinal.bmex (o : ordinal) (f : Π (a : ordinal), a < oordinal) :

The minimum excluded ordinal of a family of ordinals indexed by the set of ordinals less than some o : ordinal.{u}. This is a special case of mex over the family provided by family_of_bfamily.

This is to mex as bsup is to sup.

Equations
theorem ordinal.bmex_not_mem_brange {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
o.bmex f o.brange f
theorem ordinal.ne_bmex {o : ordinal} (f : Π (a : ordinal), a < oordinal) {i : ordinal} (hi : i < o) :
f i hi o.bmex f
theorem ordinal.bmex_le_of_ne {o : ordinal} {f : Π (a : ordinal), a < oordinal} {a : ordinal} (ha : ∀ (i : ordinal) (hi : i < o), f i hi a) :
o.bmex f a
theorem ordinal.exists_of_lt_bmex {o : ordinal} {f : Π (a : ordinal), a < oordinal} {a : ordinal} (ha : a < o.bmex f) :
∃ (i : ordinal) (hi : i < o), f i hi = a
theorem ordinal.bmex_le_blsub {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
o.bmex f o.blsub f
theorem ordinal.bmex_monotone {o o' : ordinal} {f : Π (a : ordinal), a < oordinal} {g : Π (a : ordinal), a < o'ordinal} (h : o.brange f o'.brange g) :
o.bmex f o'.bmex g
theorem ordinal.bmex_lt_ord_succ_card {o : ordinal} (f : Π (a : ordinal), a < oordinal) :

Results about injectivity and surjectivity #

theorem not_surjective_of_ordinal {α : Type u} (f : α → ordinal) :
theorem not_injective_of_ordinal {α : Type u} (f : ordinal → α) :
theorem not_surjective_of_ordinal_of_small {α : Type v} [small α] (f : α → ordinal) :
theorem not_injective_of_ordinal_of_small {α : Type v} [small α] (f : ordinal → α) :

The type of ordinals in universe u is not small.{u}. This is the type-theoretic analog of the Burali-Forti paradox.

Enumerating unbounded sets of ordinals with ordinals #

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

Enumerator function for an unbounded set of ordinals.

Equations
theorem ordinal.enum_ord_def' {S : set ordinal} (o : ordinal) :
ordinal.enum_ord S o = has_Inf.Inf (S set.Ici (o.blsub (λ (a : ordinal) (_x : a < o), ordinal.enum_ord S a)))

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

The set in enum_ord_def' is nonempty.

theorem ordinal.blsub_le_enum_ord {S : set ordinal} (hS : set.unbounded has_lt.lt S) (o : ordinal) :
o.blsub (λ (c : ordinal) (_x : c < o), ordinal.enum_ord S c) ordinal.enum_ord S o
theorem ordinal.enum_ord_def {S : set ordinal} (o : ordinal) :
ordinal.enum_ord S o = has_Inf.Inf (S {b : ordinal | ∀ (c : ordinal), c < oordinal.enum_ord S c < b})

A more workable definition for enum_ord.

theorem ordinal.enum_ord_def_nonempty {S : set ordinal} (hS : set.unbounded has_lt.lt S) {o : ordinal} :
{x : ordinal | x S ∀ (c : ordinal), c < oordinal.enum_ord S c < x}.nonempty

The set in enum_ord_def is nonempty.

@[simp]
theorem ordinal.enum_ord_succ_le {S : set ordinal} {a b : ordinal} (hS : set.unbounded has_lt.lt S) (ha : a S) (hb : ordinal.enum_ord S b < a) :
theorem ordinal.enum_ord_surjective {S : set ordinal} (hS : set.unbounded has_lt.lt S) (s : ordinal) (H : s S) :
∃ (a : ordinal), ordinal.enum_ord S a = s

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

Equations

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

Ordinal exponential #

@[protected, instance]
noncomputable def ordinal.has_pow  :

The ordinal exponential, defined by transfinite recursion.

Equations
theorem ordinal.opow_def (a b : ordinal) :
a ^ b = ite (a = 0) (1 - b) (b.limit_rec_on 1 (λ (_x IH : ordinal), IH * a) (λ (b : ordinal) (_x : b.is_limit), b.bsup))
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 ^ order.succ b = 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.left_le_opow (a : ordinal) {b : ordinal} (b1 : 0 < b) :
a a ^ b
theorem ordinal.right_le_opow {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) :
theorem ordinal.opow_add (a b c : ordinal) :
a ^ (b + c) = a ^ b * a ^ c
theorem ordinal.opow_one_add (a b : ordinal) :
a ^ (1 + b) = a * a ^ b
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
theorem ordinal.log_nonempty {b x : ordinal} (h : 1 < b) :
{o : ordinal | x < b ^ o}.nonempty

The set in the definition of log is nonempty.

theorem ordinal.log_def {b : ordinal} (b1 : 1 < b) (x : ordinal) :
ordinal.log b x = (has_Inf.Inf {o : ordinal | x < b ^ o}).pred
theorem ordinal.log_of_not_one_lt_left {b : ordinal} (b1 : ¬1 < b) (x : ordinal) :
theorem ordinal.log_of_left_le_one {b : ordinal} (b1 : b 1) (x : ordinal) :
@[simp]
theorem ordinal.log_zero_left (b : ordinal) :
@[simp]
theorem ordinal.log_zero_right (b : ordinal) :
@[simp]
theorem ordinal.log_one_left (b : ordinal) :
theorem ordinal.succ_log_def {b x : ordinal} (b1 : 1 < b) (x0 : 0 < x) :
theorem ordinal.lt_opow_succ_log_self {b : ordinal} (b1 : 1 < b) (x : ordinal) :
theorem ordinal.opow_log_le_self (b : ordinal) {x : ordinal} (x0 : 0 < x) :
b ^ ordinal.log b x x
theorem ordinal.opow_le_iff_le_log {b x c : ordinal} (b1 : 1 < b) (x0 : 0 < x) :
b ^ c x c ordinal.log b x

opow b and log b (almost) form a Galois connection.

theorem ordinal.lt_opow_iff_log_lt {b x c : ordinal} (b1 : 1 < b) (x0 : 0 < x) :
x < b ^ c ordinal.log b x < c
theorem ordinal.log_mono_right (b : ordinal) {x y : ordinal} (xy : x y) :
theorem ordinal.log_le_self (b x : ordinal) :
@[simp]
theorem ordinal.log_one_right (b : ordinal) :
theorem ordinal.mod_opow_log_lt_self {b o : ordinal} (b0 : b 0) (o0 : o 0) :
o % b ^ ordinal.log b o < o
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 * order.succ v
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 ^ order.succ u
theorem ordinal.log_opow_mul_add {b u v w : ordinal} (hb : 1 < b) (hv : 0 < v) (hvb : v < b) (hw : w < b ^ u) :
ordinal.log b (b ^ u * v + w) = u
@[simp]
theorem ordinal.log_opow {b : ordinal} (hb : 1 < b) (x : ordinal) :
ordinal.log b (b ^ x) = x
theorem ordinal.add_log_le_log_mul {x y : ordinal} (b : ordinal) (x0 : 0 < x) (y0 : 0 < y) :

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]
@[simp]
theorem ordinal.lift_nat_cast (n : ) :
theorem ordinal.type_fintype {α : Type u_1} (r : α → α → Prop) [is_well_order α r] [fintype α] :

Properties of omega #

@[simp]
theorem ordinal.lt_add_of_limit {a b c : ordinal} (h : c.is_limit) :
a < b + c ∃ (c' : ordinal) (H : c' < c), a < b + c'
theorem ordinal.lt_omega {o : ordinal} :
o < ordinal.omega ∃ (n : ), o = n
theorem ordinal.omega_le {o : ordinal} :
ordinal.omega o ∀ (n : ), n o
theorem ordinal.nat_lt_limit {o : ordinal} (h : o.is_limit) (n : ) :
n < o
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) * order.succ c' = a * order.succ c' + b) :
(a + b) * c = a * c
theorem ordinal.add_mul_succ {a b : ordinal} (c : ordinal) (ba : b + a = a) :
(a + b) * order.succ c = a * order.succ c + 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.add_le_of_forall_add_lt {a b c : ordinal} (hb : 0 < b) (h : ∀ (d : ordinal), d < ba + d < c) :
a + b c
@[simp]
theorem ordinal.sup_add_nat (o : ordinal) :
ordinal.sup (λ (n : ), o + n) = o + ordinal.omega
@[simp]
theorem ordinal.sup_mul_nat (o : ordinal) :
ordinal.sup (λ (n : ), o * n) = o * ordinal.omega
theorem ordinal.sup_opow_nat {o : ordinal} (ho : 0 < o) :
ordinal.sup (λ (n : ), o ^ n) = o ^ ordinal.omega