# 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 limitRecOn.

## 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.
• Order.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 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:

• IsLimit o: an ordinal is a limit ordinal if it is neither 0 nor a successor.
• limitRecOn 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.
• IsNormal: a function f : Ordinal → Ordinal satisfies IsNormal 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.
• enumOrd: enumerates an unbounded set of ordinals by the ordinals themselves.
• 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.

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

### Further properties of addition on ordinals #

@[simp]
Equations
CovariantClass Ordinal.{u} Ordinal.{u} (fun (x x_1 : Ordinal.{u}) => x + x_1) fun (x x_1 : Ordinal.{u}) => x < x_1
Equations
ContravariantClass Ordinal.{u} Ordinal.{u} (fun (x x_1 : Ordinal.{u}) => x + x_1) fun (x x_1 : Ordinal.{u}) => x < x_1
Equations
theorem Ordinal.add_le_add_iff_right {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (n : ) :
a + n b + n a b
theorem Ordinal.add_right_cancel {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (n : ) :
a + n = b + n a = b

### The predecessor of an ordinal #

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

Equations
Instances For
@[simp]
theorem Ordinal.pred_succ (o : Ordinal.{u_4}) :
().pred = o
theorem Ordinal.pred_lt_iff_is_succ {o : Ordinal.{u_4}} :
o.pred < o ∃ (a : Ordinal.{u_4}), o =
@[simp]
theorem Ordinal.succ_lt_of_not_succ {o : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : ¬∃ (a : Ordinal.{u_4}), o = ) :
< o b < o
theorem Ordinal.lt_pred {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
a < b.pred < b
theorem Ordinal.pred_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
a.pred b a
@[simp]
theorem Ordinal.lift_is_succ {o : Ordinal.{v}} :
(∃ (a : Ordinal.{max v u} ), ) ∃ (a : Ordinal.{v}), o =
@[simp]
theorem Ordinal.lift_pred (o : Ordinal.{v}) :
Ordinal.lift.{u, v} o.pred = ().pred

### Limit ordinals #

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

Equations
• o.IsLimit = (o 0 a < o, < o)
Instances For
theorem Ordinal.IsLimit.isSuccLimit {o : Ordinal.{u_4}} (h : o.IsLimit) :
theorem Ordinal.IsLimit.succ_lt {o : Ordinal.{u_4}} {a : Ordinal.{u_4}} (h : o.IsLimit) :
a < o < o
theorem Ordinal.not_succ_of_isLimit {o : Ordinal.{u_4}} (h : o.IsLimit) :
¬∃ (a : Ordinal.{u_4}), o =
theorem Ordinal.succ_lt_of_isLimit {o : Ordinal.{u_4}} {a : Ordinal.{u_4}} (h : o.IsLimit) :
< o a < o
theorem Ordinal.le_succ_of_isLimit {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_4}} :
o o a
theorem Ordinal.limit_le {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_4}} :
o a x < o, x a
theorem Ordinal.lt_limit {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_4}} :
a < o x < o, a < x
@[simp]
theorem Ordinal.lift_isLimit (o : Ordinal.{u_4}) :
().IsLimit o.IsLimit
theorem Ordinal.IsLimit.pos {o : Ordinal.{u_4}} (h : o.IsLimit) :
0 < o
theorem Ordinal.IsLimit.one_lt {o : Ordinal.{u_4}} (h : o.IsLimit) :
1 < o
theorem Ordinal.IsLimit.nat_lt {o : Ordinal.{u_4}} (h : o.IsLimit) (n : ) :
n < o
theorem Ordinal.zero_or_succ_or_limit (o : Ordinal.{u_4}) :
o = 0 (∃ (a : Ordinal.{u_4}), o = ) o.IsLimit
def Ordinal.limitRecOn {C : } (o : Ordinal.{u_5}) (H₁ : C 0) (H₂ : (o : Ordinal.{u_5}) → C oC ()) (H₃ : (o : Ordinal.{u_5}) → o.IsLimit((o' : Ordinal.{u_5}) → 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Ordinal.limitRecOn_zero {C : } (H₁ : C 0) (H₂ : (o : Ordinal.{u_4}) → C oC ()) (H₃ : (o : Ordinal.{u_4}) → o.IsLimit((o' : Ordinal.{u_4}) → o' < oC o')C o) :
Ordinal.limitRecOn 0 H₁ H₂ H₃ = H₁
@[simp]
theorem Ordinal.limitRecOn_succ {C : } (o : Ordinal.{u_4}) (H₁ : C 0) (H₂ : (o : Ordinal.{u_4}) → C oC ()) (H₃ : (o : Ordinal.{u_4}) → o.IsLimit((o' : Ordinal.{u_4}) → o' < oC o')C o) :
().limitRecOn H₁ H₂ H₃ = H₂ o (o.limitRecOn H₁ H₂ H₃)
@[simp]
theorem Ordinal.limitRecOn_limit {C : } (o : Ordinal.{u_4}) (H₁ : C 0) (H₂ : (o : Ordinal.{u_4}) → C oC ()) (H₃ : (o : Ordinal.{u_4}) → o.IsLimit((o' : Ordinal.{u_4}) → o' < oC o')C o) (h : o.IsLimit) :
o.limitRecOn H₁ H₂ H₃ = H₃ o h fun (x : Ordinal.{u_4}) (_h : x < o) => x.limitRecOn H₁ H₂ H₃
Equations
• o.orderTopOutSucc =
theorem Ordinal.enum_succ_eq_top {o : Ordinal.{u_4}} :
Ordinal.enum (fun (x x_1 : ()) => x < x_1) o =
theorem Ordinal.has_succ_of_type_succ_lt {α : Type u_4} {r : ααProp} [wo : ] (h : a < , ) (x : α) :
∃ (y : α), r x y
theorem Ordinal.out_no_max_of_succ_lt {o : Ordinal.{u_4}} (ho : a < o, < o) :
theorem Ordinal.bounded_singleton {α : Type u_1} {r : ααProp} [] (hr : ().IsLimit) (x : α) :
theorem Ordinal.type_subrel_lt (o : Ordinal.{u}) :
Ordinal.type (Subrel (fun (x x_1 : Ordinal.{u}) => x < x_1) {o' : Ordinal.{u} | o' < o}) =

### Normal ordinal functions #

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
Instances For
theorem Ordinal.IsNormal.limit_le {f : } (H : ) {o : Ordinal.{u_4}} :
o.IsLimit∀ {a : Ordinal.{u_5}}, f o a b < o, f b a
theorem Ordinal.IsNormal.limit_lt {f : } (H : ) {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_5}} :
a < f o b < o, a < f b
theorem Ordinal.IsNormal.strictMono {f : } (H : ) :
theorem Ordinal.IsNormal.monotone {f : } (H : ) :
theorem Ordinal.isNormal_iff_strictMono_limit (f : ) :
∀ (o : Ordinal.{u_4}), o.IsLimit∀ (a : Ordinal.{u_5}), (b < o, f b a)f o a
theorem Ordinal.IsNormal.lt_iff {f : } (H : ) {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
f a < f b a < b
theorem Ordinal.IsNormal.le_iff {f : } (H : ) {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
f a f b a b
theorem Ordinal.IsNormal.inj {f : } (H : ) {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
f a = f b a = b
theorem Ordinal.IsNormal.self_le {f : } (H : ) (a : Ordinal.{u_4}) :
a f a
theorem Ordinal.IsNormal.le_set {f : } {o : Ordinal.{u_5}} (H : ) (p : ) (p0 : p.Nonempty) (b : Ordinal.{u_4}) (H₂ : ∀ (o : Ordinal.{u_4}), b o ap, a o) :
f b o ap, f a o
theorem Ordinal.IsNormal.le_set' {α : Type u_1} {f : } {o : Ordinal.{u_5}} (H : ) (p : Set α) (p0 : p.Nonempty) (g : ) (b : Ordinal.{u_4}) (H₂ : ∀ (o : Ordinal.{u_4}), b o ap, g a o) :
f b o ap, f (g a) o
theorem Ordinal.IsNormal.trans {f : } {g : } (H₁ : ) (H₂ : ) :
theorem Ordinal.IsNormal.isLimit {f : } (H : ) {o : Ordinal.{u_4}} (l : o.IsLimit) :
(f o).IsLimit
theorem Ordinal.IsNormal.le_iff_eq {f : } (H : ) {a : Ordinal.{u_4}} :
f a a f a = a
theorem Ordinal.add_le_of_limit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : b.IsLimit) :
a + b c b' < b, a + b' c
theorem Ordinal.add_isLimit (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} :
b.IsLimit(a + b).IsLimit
theorem Ordinal.IsLimit.add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} :
b.IsLimit(a + b).IsLimit

Alias of Ordinal.add_isLimit.

### Subtraction on ordinals #

theorem Ordinal.sub_nonempty {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
{o : Ordinal.{u_4} | a b + o}.Nonempty

The set in the definition of subtraction is nonempty.

instance Ordinal.sub :

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

Equations
theorem Ordinal.sub_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} :
a - b c a b + c
theorem Ordinal.lt_sub {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} :
a < b - c c + a < b
theorem Ordinal.sub_eq_of_add_eq {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : a + b = c) :
c - a = b
theorem Ordinal.add_sub_cancel_of_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : b a) :
b + (a - b) = a
theorem Ordinal.le_sub_of_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : b a) :
c a - b b + c a
theorem Ordinal.sub_lt_of_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : b a) :
a - b < c a < b + c
Equations
@[simp]
theorem Ordinal.sub_zero (a : Ordinal.{u_4}) :
a - 0 = a
@[simp]
theorem Ordinal.zero_sub (a : Ordinal.{u_4}) :
0 - a = 0
@[simp]
theorem Ordinal.sub_self (a : Ordinal.{u_4}) :
a - a = 0
theorem Ordinal.sub_sub (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) (c : Ordinal.{u_4}) :
a - b - c = a - (b + c)
@[simp]
theorem Ordinal.add_sub_add_cancel (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) (c : Ordinal.{u_4}) :
a + b - (a + c) = b - c
theorem Ordinal.sub_isLimit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (l : a.IsLimit) (h : b < a) :
(a - b).IsLimit
@[simp]
theorem Ordinal.one_add_of_omega_le {o : Ordinal.{u_4}} (h : ) :
1 + o = o

### Multiplication of ordinals #

instance Ordinal.monoid :

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

Equations
@[simp]
theorem Ordinal.type_prod_lex {α : Type u} {β : Type u} (r : ααProp) (s : ββProp) [] [] :
Equations
Equations
@[simp]
theorem Ordinal.card_mul (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) :
(a * b).card = a.card * b.card
Equations
theorem Ordinal.mul_succ (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) :
a * = a * b + a
instance Ordinal.mul_covariantClass_le :
CovariantClass Ordinal.{u} Ordinal.{u} (fun (x x_1 : Ordinal.{u}) => x * x_1) fun (x x_1 : Ordinal.{u}) => x x_1
Equations
theorem Ordinal.le_mul_left (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (hb : 0 < b) :
a a * b
theorem Ordinal.le_mul_right (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (hb : 0 < b) :
a b * a
theorem Ordinal.mul_le_of_limit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : b.IsLimit) :
a * b c b' < b, a * b' c
theorem Ordinal.mul_isNormal {a : Ordinal.{u_4}} (h : 0 < a) :
theorem Ordinal.lt_mul_of_limit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c.IsLimit) :
a < b * c c' < c, a < b * c'
theorem Ordinal.mul_lt_mul_iff_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (a0 : 0 < a) :
a * b < a * c b < c
theorem Ordinal.mul_le_mul_iff_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (a0 : 0 < a) :
a * b a * c b c
theorem Ordinal.mul_lt_mul_of_pos_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : a < b) (c0 : 0 < c) :
c * a < c * b
theorem Ordinal.mul_pos {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h₁ : 0 < a) (h₂ : 0 < b) :
0 < a * b
theorem Ordinal.mul_ne_zero {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
a 0b 0a * b 0
theorem Ordinal.le_of_mul_le_mul_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c * a c * b) (h0 : 0 < c) :
a b
theorem Ordinal.mul_right_inj {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (a0 : 0 < a) :
a * b = a * c b = c
theorem Ordinal.mul_isLimit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (a0 : 0 < a) :
b.IsLimit(a * b).IsLimit
theorem Ordinal.mul_isLimit_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (l : a.IsLimit) (b0 : 0 < b) :
(a * b).IsLimit
theorem Ordinal.smul_eq_mul (n : ) (a : Ordinal.{u_4}) :
n a = a * n

### Division on ordinals #

theorem Ordinal.div_nonempty {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : b 0) :
{o : Ordinal.{u_4} | a < b * }.Nonempty

The set in the definition of division is nonempty.

instance Ordinal.div :

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

Equations
@[simp]
theorem Ordinal.div_zero (a : Ordinal.{u_4}) :
a / 0 = 0
theorem Ordinal.div_def (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b 0) :
a / b = sInf {o : Ordinal.{u_4} | a < b * }
theorem Ordinal.lt_mul_succ_div (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b 0) :
a < b * Order.succ (a / b)
theorem Ordinal.lt_mul_div_add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b 0) :
a < b * (a / b) + b
theorem Ordinal.div_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (b0 : b 0) :
a / b c a < b *
theorem Ordinal.lt_div {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c 0) :
a < b / c c * b
theorem Ordinal.div_pos {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c 0) :
0 < b / c c b
theorem Ordinal.le_div {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (c0 : c 0) :
a b / c c * a b
theorem Ordinal.div_lt {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (b0 : b 0) :
a / b < c a < b * c
theorem Ordinal.div_le_of_le_mul {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : a b * c) :
a / b c
theorem Ordinal.mul_lt_of_lt_div {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} :
a < b / cc * a < b
@[simp]
theorem Ordinal.zero_div (a : Ordinal.{u_4}) :
0 / a = 0
theorem Ordinal.mul_add_div (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (b0 : b 0) (c : Ordinal.{u_4}) :
(b * a + c) / b = a + c / b
theorem Ordinal.div_eq_zero_of_lt {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : a < b) :
a / b = 0
@[simp]
theorem Ordinal.mul_div_cancel (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (b0 : b 0) :
b * a / b = a
@[simp]
theorem Ordinal.div_one (a : Ordinal.{u_4}) :
a / 1 = a
@[simp]
theorem Ordinal.div_self {a : Ordinal.{u_4}} (h : a 0) :
a / a = 1
theorem Ordinal.mul_sub (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) (c : Ordinal.{u_4}) :
a * (b - c) = a * b - a * c
theorem Ordinal.isLimit_add_iff {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
(a + b).IsLimit b.IsLimit b = 0 a.IsLimit
theorem Ordinal.dvd_add_iff {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} :
a b(a b + c a c)
theorem Ordinal.div_mul_cancel {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
a 0a ba * (b / a) = b
theorem Ordinal.le_of_dvd {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
b 0a ba b
theorem Ordinal.dvd_antisymm {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h₁ : a b) (h₂ : b a) :
a = b
Equations
instance Ordinal.mod :

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

Equations
theorem Ordinal.mod_def (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) :
a % b = a - b * (a / b)
@[simp]
theorem Ordinal.mod_zero (a : Ordinal.{u_4}) :
a % 0 = a
theorem Ordinal.mod_eq_of_lt {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : a < b) :
a % b = a
@[simp]
theorem Ordinal.zero_mod (b : Ordinal.{u_4}) :
0 % b = 0
theorem Ordinal.div_add_mod (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) :
b * (a / b) + a % b = a
theorem Ordinal.mod_lt (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b 0) :
a % b < b
@[simp]
theorem Ordinal.mod_self (a : Ordinal.{u_4}) :
a % a = 0
@[simp]
theorem Ordinal.mod_one (a : Ordinal.{u_4}) :
a % 1 = 0
theorem Ordinal.dvd_of_mod_eq_zero {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (H : a % b = 0) :
b a
theorem Ordinal.mod_eq_zero_of_dvd {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (H : b a) :
a % b = 0
@[simp]
theorem Ordinal.mul_add_mod_self (x : Ordinal.{u_4}) (y : Ordinal.{u_4}) (z : Ordinal.{u_4}) :
(x * y + z) % x = z % x
@[simp]
theorem Ordinal.mul_mod (x : Ordinal.{u_4}) (y : Ordinal.{u_4}) :
x * y % x = 0
theorem Ordinal.mod_mod_of_dvd (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c b) :
a % b % c = a % c
@[simp]
theorem Ordinal.mod_mod (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) :
a % b % b = a % b

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

def Ordinal.bfamilyOfFamily' {α : Type u_1} {ι : Type u} (r : ιιProp) [] (f : ια) (a : Ordinal.{u}) :
α

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

Equations
Instances For
def Ordinal.bfamilyOfFamily {α : Type u_1} {ι : Type u} :
(ια)(a : Ordinal.{u}) → a < Ordinal.type WellOrderingRelα

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
Instances For
def Ordinal.familyOfBFamily' {α : Type u_1} {ι : Type u} (r : ιιProp) [] {o : Ordinal.{u}} (ho : ) (f : (a : Ordinal.{u}) → a < oα) :
ια

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

Equations
• = f ()
Instances For
def Ordinal.familyOfBFamily {α : Type u_1} (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < 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
Instances For
@[simp]
theorem Ordinal.bfamilyOfFamily'_typein {α : Type u_1} {ι : Type u_4} (r : ιιProp) [] (f : ια) (i : ι) :
= f i
@[simp]
theorem Ordinal.bfamilyOfFamily_typein {α : Type u_1} {ι : Type u_4} (f : ια) (i : ι) :
Ordinal.bfamilyOfFamily f (Ordinal.typein WellOrderingRel i) = f i
@[simp]
theorem Ordinal.familyOfBFamily'_enum {α : Type u_1} {ι : Type u} (r : ιιProp) [] {o : Ordinal.{u}} (ho : ) (f : (a : Ordinal.{u}) → a < oα) (i : Ordinal.{u}) (hi : i < o) :
Ordinal.familyOfBFamily' r ho f (Ordinal.enum r i ) = f i hi
@[simp]
theorem Ordinal.familyOfBFamily_enum {α : Type u_1} (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < oα) (i : Ordinal.{u_4}) (hi : i < o) :
o.familyOfBFamily f (Ordinal.enum (fun (x x_1 : ()) => x < x_1) i ) = f i hi
def Ordinal.brange {α : Type u_1} (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < oα) :
Set α

The range of a family indexed by ordinals.

Equations
Instances For
theorem Ordinal.mem_brange {α : Type u_1} {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < oα} {a : α} :
a o.brange f ∃ (i : Ordinal.{u_4}) (hi : i < o), f i hi = a
theorem Ordinal.mem_brange_self {α : Type u_1} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < oα) (i : Ordinal.{u_4}) (hi : i < o) :
f i hi o.brange f
@[simp]
theorem Ordinal.range_familyOfBFamily' {α : Type u_1} {ι : Type u} (r : ιιProp) [] {o : Ordinal.{u}} (ho : ) (f : (a : Ordinal.{u}) → a < oα) :
Set.range () = o.brange f
@[simp]
theorem Ordinal.range_familyOfBFamily {α : Type u_1} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < oα) :
Set.range (o.familyOfBFamily f) = o.brange f
@[simp]
theorem Ordinal.brange_bfamilyOfFamily' {α : Type u_1} {ι : Type u} (r : ιιProp) [] (f : ια) :
().brange () =
@[simp]
theorem Ordinal.brange_bfamilyOfFamily {α : Type u_1} {ι : Type u} (f : ια) :
(Ordinal.type WellOrderingRel).brange =
@[simp]
theorem Ordinal.brange_const {α : Type u_1} {o : Ordinal.{u_4}} (ho : o 0) {c : α} :
(o.brange fun (x : Ordinal.{u_4}) (x : x < o) => c) = {c}
theorem Ordinal.comp_bfamilyOfFamily' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ιιProp) [] (f : ια) (g : αβ) :
(fun (i : Ordinal.{u}) (hi : ) => g ()) = Ordinal.bfamilyOfFamily' r (g f)
theorem Ordinal.comp_bfamilyOfFamily {α : Type u_1} {β : Type u_2} {ι : Type u} (f : ια) (g : αβ) :
(fun (i : Ordinal.{u}) (hi : i < Ordinal.type WellOrderingRel) => g ()) = Ordinal.bfamilyOfFamily (g f)
theorem Ordinal.comp_familyOfBFamily' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ιιProp) [] {o : Ordinal.{u}} (ho : ) (f : (a : Ordinal.{u}) → a < oα) (g : αβ) :
g = Ordinal.familyOfBFamily' r ho fun (i : Ordinal.{u}) (hi : i < o) => g (f i hi)
theorem Ordinal.comp_familyOfBFamily {α : Type u_1} {β : Type u_2} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < oα) (g : αβ) :
g o.familyOfBFamily f = o.familyOfBFamily fun (i : Ordinal.{u_4}) (hi : i < o) => g (f i hi)

### Supremum of a family of ordinals #

def Ordinal.sup {ι : Type u} (f : ) :

The supremum of a family of ordinals

Equations
Instances For
@[simp]
theorem Ordinal.sSup_eq_sup {ι : Type u} (f : ) :
sSup () =
theorem Ordinal.bddAbove_range {ι : Type u} (f : ) :

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} (f : ) (i : ι) :
f i
theorem Ordinal.sup_le_iff {ι : Type u} {f : } {a : Ordinal.{max u v} } :
a ∀ (i : ι), f i a
theorem Ordinal.sup_le {ι : Type u} {f : } {a : Ordinal.{max u v} } :
(∀ (i : ι), f i a) a
theorem Ordinal.lt_sup {ι : Type u} {f : } {a : Ordinal.{max u v} } :
a < ∃ (i : ι), a < f i
theorem Ordinal.ne_sup_iff_lt_sup {ι : Type u} {f : } :
(∀ (i : ι), f i ) ∀ (i : ι), f i <
theorem Ordinal.sup_not_succ_of_ne_sup {ι : Type u} {f : } (hf : ∀ (i : ι), f i ) {a : Ordinal.{max u v} } (hao : a < ) :
@[simp]
theorem Ordinal.sup_eq_zero_iff {ι : Type u} {f : } :
= 0 ∀ (i : ι), f i = 0
theorem Ordinal.IsNormal.sup {f : } (H : ) {ι : Type u} (g : ) [] :
f () = Ordinal.sup (f g)
@[simp]
theorem Ordinal.sup_empty {ι : Type u_4} [] (f : ) :
= 0
@[simp]
theorem Ordinal.sup_const {ι : Type u_4} [_hι : ] :
(Ordinal.sup fun (x : ι) => o) = o
@[simp]
theorem Ordinal.sup_unique {ι : Type u_4} [] (f : ) :
= f default
theorem Ordinal.sup_le_of_range_subset {ι : Type u} {ι' : Type v} {f : } {g : } (h : ) :
theorem Ordinal.sup_eq_of_range_eq {ι : Type u} {ι' : Type v} {f : } {g : } (h : ) :
@[simp]
theorem Ordinal.sup_sum {α : Type u} {β : Type v} (f : ) :
= max (Ordinal.sup fun (a : α) => f ()) (Ordinal.sup fun (b : β) => f ())
theorem Ordinal.unbounded_range_of_sup_ge {α : Type u} {β : Type u} (r : ααProp) [] (f : βα) (h : Ordinal.sup ()) :
theorem Ordinal.le_sup_shrink_equiv {s : } (hs : ) (a : Ordinal.{u}) (ha : a s) :
a Ordinal.sup fun (x : ) => (().symm x)
Equations
• =
Equations
• =
theorem Ordinal.bddAbove_of_small (s : ) [h : ] :
theorem Ordinal.sup_eq_sSup {s : } (hs : ) :
(Ordinal.sup fun (x : ) => (().symm x)) = sSup s
theorem Ordinal.sSup_ord {s : } (hs : ) :
(sSup s).ord = sSup ()
theorem Ordinal.iSup_ord {ι : Sort u_4} {f : } (hf : ) :
(iSup f).ord = ⨆ (i : ι), (f i).ord
theorem Ordinal.sup_eq_sup {ι : Type u} {ι' : Type u} (r : ιιProp) (r' : ι'ι'Prop) [] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : ) (ho' : = o) (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
def Ordinal.bsup (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :

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

Equations
Instances For
@[simp]
theorem Ordinal.sup_eq_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
Ordinal.sup (o.familyOfBFamily f) = o.bsup f
@[simp]
theorem Ordinal.sup_eq_bsup' {o : Ordinal.{u}} {ι : Type u} (r : ιιProp) [] (ho : ) (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
Ordinal.sup () = o.bsup f
@[simp]
theorem Ordinal.sSup_eq_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
sSup (o.brange f) = o.bsup f
@[simp]
theorem Ordinal.bsup_eq_sup' {ι : Type u} (r : ιιProp) [] (f : ) :
().bsup () =
theorem Ordinal.bsup_eq_bsup {ι : Type u} (r : ιιProp) (r' : ιιProp) [] [IsWellOrder ι r'] (f : ) :
().bsup () = ().bsup ()
@[simp]
theorem Ordinal.bsup_eq_sup {ι : Type u} (f : ) :
(Ordinal.type WellOrderingRel).bsup =
theorem Ordinal.bsup_congr {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o₁Ordinal.{max u v} ) (ho : o₁ = o₂) :
o₁.bsup f = o₂.bsup fun (a : Ordinal.{u}) (h : a < o₂) => f a
theorem Ordinal.bsup_le_iff {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } {a : Ordinal.{max u v} } :
o.bsup f a ∀ (i : Ordinal.{u}) (h : i < o), f i h a
theorem Ordinal.bsup_le {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v} } {a : Ordinal.{max u v} } :
(∀ (i : Ordinal.{u}) (h : i < o), f i h a)o.bsup f a
theorem Ordinal.le_bsup {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → ) (i : Ordinal.{u_4}) (h : i < o) :
f i h o.bsup f
theorem Ordinal.lt_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) {a : Ordinal.{max u v} } :
a < o.bsup f ∃ (i : Ordinal.{u}) (hi : i < o), a < f i hi
theorem Ordinal.IsNormal.bsup {f : } (H : ) {o : Ordinal.{u}} (g : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
o 0f (o.bsup g) = o.bsup fun (a : Ordinal.{u}) (h : a < o) => f (g a h)
theorem Ordinal.lt_bsup_of_ne_bsup {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } :
(∀ (i : Ordinal.{u}) (h : i < o), f i h o.bsup f) ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f
theorem Ordinal.bsup_not_succ_of_ne_bsup {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } (hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h o.bsup f) (a : Ordinal.{max u v} ) :
a < o.bsup f < o.bsup f
@[simp]
theorem Ordinal.bsup_eq_zero_iff {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → } :
o.bsup f = 0 ∀ (i : Ordinal.{u_4}) (hi : i < o), f i hi = 0
theorem Ordinal.lt_bsup_of_limit {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → } (hf : ∀ {a a' : Ordinal.{u_4}} (ha : a < o) (ha' : a' < o), a < a'f a ha < f a' ha') (ho : a < o, < o) (i : Ordinal.{u_4}) (h : i < o) :
f i h < o.bsup f
theorem Ordinal.bsup_succ_of_mono {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → } (hf : ∀ {i j : Ordinal.{u_4}} (hi : i < ) (hj : j < ), i jf i hi f j hj) :
().bsup f = f o
@[simp]
theorem Ordinal.bsup_zero (f : (a : Ordinal.{u_4}) → ) :
= 0
theorem Ordinal.bsup_const {o : Ordinal.{u}} (ho : o 0) (a : Ordinal.{max u v} ) :
(o.bsup fun (x : Ordinal.{u}) (x : x < o) => a) = a
@[simp]
theorem Ordinal.bsup_one (f : (a : Ordinal.{u_4}) → ) :
= f 0
theorem Ordinal.bsup_le_of_brange_subset {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → } {g : (a : Ordinal.{v}) → } (h : o.brange f o'.brange g) :
o.bsup f o'.bsup g
theorem Ordinal.bsup_eq_of_brange_eq {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → } {g : (a : Ordinal.{v}) → } (h : o.brange f = o'.brange g) :
o.bsup f = o'.bsup g
def Ordinal.lsub {ι : Type u_4} (f : ) :

The least strict upper bound of a family of ordinals.

Equations
Instances For
@[simp]
theorem Ordinal.sup_eq_lsub {ι : Type u} (f : ) :
Ordinal.sup (Order.succ f) =
theorem Ordinal.lsub_le_iff {ι : Type u} {f : } {a : Ordinal.{max v u} } :
∀ (i : ι), f i < a
theorem Ordinal.lsub_le {ι : Type u_4} {f : } :
(∀ (i : ι), f i < a)
theorem Ordinal.lt_lsub {ι : Type u_4} (f : ) (i : ι) :
f i <
theorem Ordinal.lt_lsub_iff {ι : Type u} {f : } {a : Ordinal.{max v u} } :
∃ (i : ι), a f i
theorem Ordinal.sup_le_lsub {ι : Type u} (f : ) :
theorem Ordinal.lsub_le_sup_succ {ι : Type u} (f : ) :
theorem Ordinal.sup_succ_le_lsub {ι : Type u} (f : ) :
∃ (i : ι), f i =
theorem Ordinal.sup_succ_eq_lsub {ι : Type u} (f : ) :
∃ (i : ι), f i =
theorem Ordinal.sup_eq_lsub_iff_succ {ι : Type u} (f : ) :
a < ,
theorem Ordinal.sup_eq_lsub_iff_lt_sup {ι : Type u} (f : ) :
∀ (i : ι), f i <
@[simp]
theorem Ordinal.lsub_empty {ι : Type u_4} [h : ] (f : ) :
theorem Ordinal.lsub_pos {ι : Type u} [h : ] (f : ) :
@[simp]
theorem Ordinal.lsub_eq_zero_iff {ι : Type u} (f : ) :
@[simp]
theorem Ordinal.lsub_const {ι : Type u_4} [] :
(Ordinal.lsub fun (x : ι) => o) =
@[simp]
theorem Ordinal.lsub_unique {ι : Type u_4} [] (f : ) :
= Order.succ (f default)
theorem Ordinal.lsub_le_of_range_subset {ι : Type u} {ι' : Type v} {f : } {g : } (h : ) :
theorem Ordinal.lsub_eq_of_range_eq {ι : Type u} {ι' : Type v} {f : } {g : } (h : ) :
@[simp]
theorem Ordinal.lsub_sum {α : Type u} {β : Type v} (f : ) :
= max (Ordinal.lsub fun (a : α) => f ()) (Ordinal.lsub fun (b : β) => f ())
theorem Ordinal.lsub_not_mem_range {ι : Type u} (f : ) :
theorem Ordinal.nonempty_compl_range {ι : Type u} (f : ) :
().Nonempty
@[simp]
theorem Ordinal.lsub_typein (o : Ordinal.{u}) :
Ordinal.lsub (Ordinal.typein fun (x x_1 : ()) => x < x_1) = o
theorem Ordinal.sup_typein_limit {o : Ordinal.{u}} (ho : a < o, < o) :
Ordinal.sup (Ordinal.typein fun (x x_1 : ()) => x < x_1) = o
@[simp]
theorem Ordinal.sup_typein_succ {o : Ordinal.{u}} :
Ordinal.sup (Ordinal.typein fun (x x_1 : ()) => x < x_1) = o
def Ordinal.blsub (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :

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
Instances For
@[simp]
theorem Ordinal.bsup_eq_blsub (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
(o.bsup fun (a : Ordinal.{u}) (ha : a < o) => Order.succ (f a ha)) = o.blsub f
theorem Ordinal.lsub_eq_blsub' {ι : Type u} (r : ιιProp) [] {o : Ordinal.{u}} (ho : ) (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
Ordinal.lsub () = o.blsub f
theorem Ordinal.lsub_eq_lsub {ι : Type u} {ι' : Type u} (r : ιιProp) (r' : ι'ι'Prop) [] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : ) (ho' : = o) (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
@[simp]
theorem Ordinal.lsub_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
Ordinal.lsub (o.familyOfBFamily f) = o.blsub f
@[simp]
theorem Ordinal.blsub_eq_lsub' {ι : Type u} (r : ιιProp) [] (f : ) :
().blsub () =
theorem Ordinal.blsub_eq_blsub {ι : Type u} (r : ιιProp) (r' : ιιProp) [] [IsWellOrder ι r'] (f : ) :
().blsub () = ().blsub ()
@[simp]
theorem Ordinal.blsub_eq_lsub {ι : Type u} (f : ) :
(Ordinal.type WellOrderingRel).blsub =
theorem Ordinal.blsub_congr {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o₁Ordinal.{max u v} ) (ho : o₁ = o₂) :
o₁.blsub f = o₂.blsub fun (a : Ordinal.{u}) (h : a < o₂) => f a
theorem Ordinal.blsub_le_iff {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } {a : Ordinal.{max u v} } :
o.blsub f a ∀ (i : Ordinal.{u}) (h : i < o), f i h < a
theorem Ordinal.blsub_le {o : Ordinal.{u_4}} {f : (b : Ordinal.{u_4}) → } :
(∀ (i : Ordinal.{u_4}) (h : i < o), f i h < a)o.blsub f a
theorem Ordinal.lt_blsub {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → ) (i : Ordinal.{u_4}) (h : i < o) :
f i h < o.blsub f
theorem Ordinal.lt_blsub_iff {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v} } {a : Ordinal.{max u v} } :
a < o.blsub f ∃ (i : Ordinal.{u}) (hi : i < o), a f i hi
theorem Ordinal.bsup_le_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
o.bsup f o.blsub f
theorem Ordinal.blsub_le_bsup_succ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
o.blsub f Order.succ (o.bsup f)
theorem Ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
o.bsup f = o.blsub f Order.succ (o.bsup f) = o.blsub f
theorem Ordinal.bsup_succ_le_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
Order.succ (o.bsup f) o.blsub f ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o.bsup f
theorem Ordinal.bsup_succ_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
Order.succ (o.bsup f) = o.blsub f ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o.bsup f
theorem Ordinal.bsup_eq_blsub_iff_succ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
o.bsup f = o.blsub f a < o.blsub f, < o.blsub f
theorem Ordinal.bsup_eq_blsub_iff_lt_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
o.bsup f = o.blsub f ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < o.bsup f
theorem Ordinal.bsup_eq_blsub_of_lt_succ_limit {o : Ordinal.{u}} (ho : o.IsLimit) {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } (hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f () ) :
o.bsup f = o.blsub f
theorem Ordinal.blsub_succ_of_mono {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → } (hf : ∀ {i j : Ordinal.{u}} (hi : i < ) (hj : j < ), i jf i hi f j hj) :
().blsub f = Order.succ (f o )
@[simp]
theorem Ordinal.blsub_eq_zero_iff {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → } :
o.blsub f = 0 o = 0
@[simp]
theorem Ordinal.blsub_zero (f : (a : Ordinal.{u_4}) → ) :
= 0
theorem Ordinal.blsub_pos {o : Ordinal.{u_4}} (ho : 0 < o) (f : (a : Ordinal.{u_4}) → ) :
0 < o.blsub f
theorem Ordinal.blsub_type {α : Type u} (r : ααProp) [] (f : (a : Ordinal.{u}) → ) :
().blsub f = Ordinal.lsub fun (a : α) => f ()
theorem Ordinal.blsub_const {o : Ordinal.{u}} (ho : o 0) (a : Ordinal.{max u v} ) :
(o.blsub fun (x : Ordinal.{u}) (x : x < o) => a) =
@[simp]
theorem Ordinal.blsub_one (f : (a : Ordinal.{u_4}) → ) :
= Order.succ (f 0 )
@[simp]
theorem Ordinal.blsub_id (o : Ordinal.{u}) :
(o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => x) = o
theorem Ordinal.bsup_id_limit {o : Ordinal.{u}} :
(a < o, < o)(o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => x) = o
@[simp]
theorem Ordinal.bsup_id_succ (o : Ordinal.{u}) :
(().bsup fun (x : Ordinal.{u}) (x_1 : x < ) => x) = o
theorem Ordinal.blsub_le_of_brange_subset {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → } {g : (a : Ordinal.{v}) → } (h : o.brange f o'.brange g) :
o.blsub f o'.blsub g
theorem Ordinal.blsub_eq_of_brange_eq {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → } {g : (a : Ordinal.{v}) → } (h : {o_1 : Ordinal.{max (max u v) w} | ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o_1} = {o : Ordinal.{max (max u v) w} | ∃ (i : Ordinal.{v}) (hi : i < o'), g i hi = o}) :
o.blsub f = o'.blsub g
theorem Ordinal.bsup_comp {o : Ordinal.{max u v} } {o' : Ordinal.{max u v} } {f : (a : Ordinal.{max u v} ) → a < oOrdinal.{max u v w} } (hf : ∀ {i j : Ordinal.{max u v} } (hi : i < o) (hj : j < o), i jf i hi f j hj) {g : (a : Ordinal.{max u v} ) → a < o'Ordinal.{max u v} } (hg : o'.blsub g = o) :
(o'.bsup fun (a : Ordinal.{max u v} ) (ha : a < o') => f (g a ha) ) = o.bsup f
theorem Ordinal.blsub_comp {o : Ordinal.{max u v} } {o' : Ordinal.{max u v} } {f : (a : Ordinal.{max u v} ) → a < oOrdinal.{max u v w} } (hf : ∀ {i j : Ordinal.{max u v} } (hi : i < o) (hj : j < o), i jf i hi f j hj) {g : (a : Ordinal.{max u v} ) → a < o'Ordinal.{max u v} } (hg : o'.blsub g = o) :
(o'.blsub fun (a : Ordinal.{max u v} ) (ha : a < o') => f (g a ha) ) = o.blsub f
theorem Ordinal.IsNormal.bsup_eq {f : } (H : ) {o : Ordinal.{u}} (h : o.IsLimit) :
(o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o
theorem Ordinal.IsNormal.blsub_eq {f : } (H : ) {o : Ordinal.{u}} (h : o.IsLimit) :
(o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o
theorem Ordinal.isNormal_iff_lt_succ_and_bsup_eq {f : } :
(∀ (a : Ordinal.{u}), f a < f ()) ∀ (o : Ordinal.{u}), o.IsLimit(o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o
theorem Ordinal.isNormal_iff_lt_succ_and_blsub_eq {f : } :
(∀ (a : Ordinal.{u}), f a < f ()) ∀ (o : Ordinal.{u}), o.IsLimit(o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o
theorem Ordinal.IsNormal.eq_iff_zero_and_succ {f : } {g : } (hf : ) (hg : ) :
f = g f 0 = g 0 ∀ (a : Ordinal.{u}), f a = g af () = g ()
def Ordinal.blsub₂ (o₁ : Ordinal.{u_4}) (o₂ : Ordinal.{u_5}) (op : {a : Ordinal.{u_4}} → a < o₁{b : Ordinal.{u_5}} → ) :

A two-argument version of Ordinal.blsub. We don't develop a full API for this, since it's only used in a handful of existence results.

Equations
• o₁.blsub₂ o₂ op = Ordinal.lsub fun (x : () × ()) => op
Instances For
theorem Ordinal.lt_blsub₂ {o₁ : Ordinal.{u_4}} {o₂ : Ordinal.{u_5}} (op : {a : Ordinal.{u_4}} → a < o₁{b : Ordinal.{u_5}} → ) {a : Ordinal.{u_4}} {b : Ordinal.{u_5}} (ha : a < o₁) (hb : b < o₂) :
op ha hb < o₁.blsub₂ o₂ fun {a : Ordinal.{u_4}} => op

### Minimum excluded ordinals #

def Ordinal.mex {ι : Type u} (f : ) :

The minimum excluded ordinal in a family of ordinals.

Equations
Instances For
theorem Ordinal.mex_not_mem_range {ι : Type u} (f : ) :
theorem Ordinal.le_mex_of_forall {ι : Type u} {f : } {a : Ordinal.{max u v} } (H : b < a, ∃ (i : ι), f i = b) :
a
theorem Ordinal.ne_mex {ι : Type u} (f : ) (i : ι) :
f i
theorem Ordinal.mex_le_of_ne {ι : Type u_4} {f : } (ha : ∀ (i : ι), f i a) :
a
theorem Ordinal.exists_of_lt_mex {ι : Type u_4} {f : } (ha : a < ) :
∃ (i : ι), f i = a
theorem Ordinal.mex_le_lsub {ι : Type u} (f : ) :
theorem Ordinal.mex_monotone {α : Type u} {β : Type u} {f : } {g : } (h : ) :
theorem Ordinal.mex_lt_ord_succ_mk {ι : Type u} (f : ) :
< ().ord
def Ordinal.bmex (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → ) :

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

This is to mex as bsup is to sup.

Equations
Instances For
theorem Ordinal.bmex_not_mem_brange {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → ) :
o.bmex fo.brange f
theorem Ordinal.le_bmex_of_forall {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → ) (H : b < a, ∃ (i : Ordinal.{u_4}) (hi : i < o), f i hi = b) :
a o.bmex f
theorem Ordinal.ne_bmex {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) {i : Ordinal.{u}} (hi : i < o) :
f i hi o.bmex f
theorem Ordinal.bmex_le_of_ne {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → } (ha : ∀ (i : Ordinal.{u_4}) (hi : i < o), f i hi a) :
o.bmex f a
theorem Ordinal.exists_of_lt_bmex {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → } (ha : a < o.bmex f) :
∃ (i : Ordinal.{u_4}) (hi : i < o), f i hi = a
theorem Ordinal.bmex_le_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
o.bmex f o.blsub f
theorem Ordinal.bmex_monotone {o : Ordinal.{u}} {o' : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } {g : (a : Ordinal.{u}) → a < o'Ordinal.{max u v} } (h : o.brange f o'.brange g) :
o.bmex f o'.bmex g
theorem Ordinal.bmex_lt_ord_succ_card {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{u}) :
o.bmex f < (Order.succ o.card).ord

### Results about injectivity and surjectivity #

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

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 #

def Ordinal.enumOrd (S : ) :

Enumerator function for an unbounded set of ordinals.

Equations
Instances For
theorem Ordinal.enumOrd_def' {S : } (o : Ordinal.{u}) :
= sInf (S Set.Ici (o.blsub fun (a : Ordinal.{u}) (x : a < o) => ))

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

theorem Ordinal.enumOrd_def'_nonempty {S : } (hS : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) S) (a : Ordinal.{u}) :
(S ).Nonempty

The set in enumOrd_def' is nonempty.

theorem Ordinal.enumOrd_mem {S : } (hS : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) S) (o : Ordinal.{u}) :
S
theorem Ordinal.blsub_le_enumOrd {S : } (hS : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) S) (o : Ordinal.{u}) :
(o.blsub fun (c : Ordinal.{u}) (x : c < o) => )
theorem Ordinal.enumOrd_strictMono {S : } (hS : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) S) :
theorem Ordinal.enumOrd_def {S : } (o : Ordinal.{u}) :
= sInf (S {b : Ordinal.{u} | c < o, < b})

A more workable definition for enumOrd.

theorem Ordinal.enumOrd_def_nonempty {S : } (hS : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) S) {o : Ordinal.{u}} :
{x : Ordinal.{u} | x S c < o, < x}.Nonempty

The set in enumOrd_def is nonempty.

@[simp]
theorem Ordinal.enumOrd_range {f : } (hf : ) :
@[simp]
@[simp]
theorem Ordinal.enumOrd_zero {S : } :
= sInf S
theorem Ordinal.enumOrd_succ_le {S : } {a : Ordinal.{u}} {b : Ordinal.{u}} (hS : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) S) (ha : a S) (hb : < a) :
a
theorem Ordinal.enumOrd_le_of_subset {S : } {T : } (hS : Set.Unbounded (fun (x x_1 : Ordinal.{u_1}) => x < x_1) S) (hST : S T) (a : Ordinal.{u_1}) :
theorem Ordinal.enumOrd_surjective {S : } (hS : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) S) (s : Ordinal.{u}) :
s S∃ (a : Ordinal.{u}), = s
def Ordinal.enumOrdOrderIso {S : } (hS : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) S) :

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

Equations
Instances For
theorem Ordinal.range_enumOrd {S : } (hS : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) S) :
theorem Ordinal.eq_enumOrd {S : } (f : ) (hS : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) S) :
= S

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

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

@[simp]
theorem Ordinal.one_add_natCast (m : ) :
1 + m = ()
theorem Ordinal.one_add_nat_cast (m : ) :
1 + m = ()

Alias of Ordinal.one_add_natCast.

@[simp]
theorem Ordinal.one_add_ofNat (m : ) [m.AtLeastTwo] :
1 + =
@[simp]
theorem Ordinal.natCast_mul (m : ) (n : ) :
(m * n) = m * n
@[deprecated Ordinal.natCast_mul]
theorem Ordinal.nat_cast_mul (m : ) (n : ) :
(m * n) = m * n

Alias of Ordinal.natCast_mul.

theorem Ordinal.natCast_le {m : } {n : } :
m n m n

Alias of Nat.cast_le, specialized to Ordinal -

@[deprecated Ordinal.natCast_le]
theorem Ordinal.nat_cast_le {m : } {n : } :
m n m n

Alias of Ordinal.natCast_le.

Alias of Nat.cast_le, specialized to Ordinal -

theorem Ordinal.natCast_inj {m : } {n : } :
m = n m = n

Alias of Nat.cast_inj, specialized to Ordinal -

@[deprecated Ordinal.natCast_inj]
theorem Ordinal.nat_cast_inj {m : } {n : } :
m = n m = n

Alias of Ordinal.natCast_inj.

Alias of Nat.cast_inj, specialized to Ordinal -

instance Ordinal.charZero :
Equations
theorem Ordinal.natCast_lt {m : } {n : } :
m < n m < n

Alias of Nat.cast_lt, specialized to Ordinal -

@[deprecated Ordinal.natCast_lt]
theorem Ordinal.nat_cast_lt {m : } {n : } :
m < n m < n

Alias of Ordinal.natCast_lt.

Alias of Nat.cast_lt, specialized to Ordinal -

theorem Ordinal.natCast_eq_zero {n : } :
n = 0 n = 0

Alias of Nat.cast_eq_zero, specialized to Ordinal -

@[deprecated Ordinal.natCast_eq_zero]
theorem Ordinal.nat_cast_eq_zero {n : } :
n = 0 n = 0

Alias of Ordinal.natCast_eq_zero.

Alias of Nat.cast_eq_zero, specialized to Ordinal -

theorem Ordinal.natCast_ne_zero {n : } :
n 0 n 0

Alias of Nat.cast_eq_zero, specialized to Ordinal -

@[deprecated Ordinal.natCast_ne_zero]
theorem Ordinal.nat_cast_ne_zero {n : } :
n 0 n 0

Alias of Ordinal.natCast_ne_zero.

Alias of Nat.cast_eq_zero, specialized to Ordinal -

theorem Ordinal.natCast_pos {n : } :
0 < n 0 < n

Alias of Nat.cast_pos', specialized to Ordinal -

@[deprecated Ordinal.natCast_pos]
theorem Ordinal.nat_cast_pos {n : } :
0 < n 0 < n

Alias of Ordinal.natCast_pos.

Alias of Nat.cast_pos', specialized to Ordinal -

@[simp]
theorem Ordinal.natCast_sub (m : ) (n : ) :
(m - n) = m - n
@[deprecated Ordinal.natCast_sub]
theorem Ordinal.nat_cast_sub (m : ) (n : ) :
(m - n) = m - n

Alias of Ordinal.natCast_sub.

@[simp]
theorem Ordinal.natCast_div (m : ) (n : ) :
(m / n) = m / n
@[deprecated Ordinal.natCast_div]
theorem Ordinal.nat_cast_div (m : ) (n : ) :
(m / n) = m / n

Alias of Ordinal.natCast_div.

@[simp]
theorem Ordinal.natCast_mod (m : ) (n : ) :
(m % n) = m % n
@[deprecated Ordinal.natCast_mod]
theorem Ordinal.nat_cast_mod (m : ) (n : ) :
(m % n) = m % n

Alias of Ordinal.natCast_mod.

@[simp]
theorem Ordinal.lift_natCast (n : ) :
= n
@[deprecated Ordinal.lift_natCast]
theorem Ordinal.lift_nat_cast (n : ) :
= n

Alias of Ordinal.lift_natCast.

@[simp]
theorem Ordinal.lift_ofNat (n : ) [n.AtLeastTwo] :

### Properties of omega#

@[simp]
@[simp]
theorem Cardinal.add_one_of_aleph0_le {c : Cardinal.{u_1}} (h : ) :
c + 1 = c
theorem Ordinal.lt_add_of_limit {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} (h : c.IsLimit) :
a < b + c c' < c, a < b + c'
theorem Ordinal.lt_omega {o : Ordinal.{u_1}} :
∃ (n : ), o = n
theorem Ordinal.omega_le {o : Ordinal.{u_1}} :
∀ (n : ), n o
@[deprecated Ordinal.sup_natCast]

Alias of Ordinal.sup_natCast.

theorem Ordinal.nat_lt_limit {o : Ordinal.{u_1}} (h : o.IsLimit) (n : ) :
n < o
theorem Ordinal.omega_le_of_isLimit {o : Ordinal.{u_1}} (h : o.IsLimit) :
theorem Ordinal.add_mul_limit_aux {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (ba : b + a = a) (l : c.IsLimit) (IH : c' < c, (a + b) * = a * + b) :
(a + b) * c = a * c
theorem Ordinal.add_mul_succ {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (c : Ordinal.{u_1}) (ba : b + a = a) :
(a + b) * = a * + b
theorem Ordinal.add_mul_limit {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (ba : b + a = a) (l : c.IsLimit) :
(a + b) * c = a * c
theorem Ordinal.add_le_of_forall_add_lt {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (hb : 0 < b) (h : d < b, a + d < c) :
a + b c
theorem Ordinal.IsNormal.apply_omega {f : } (hf : ) :
Ordinal.sup (f Nat.cast) =
@[simp]
theorem Ordinal.sup_add_nat (o : Ordinal.{u_1}) :
(Ordinal.sup fun (n : ) => o + n) =
@[simp]
theorem Ordinal.sup_mul_nat (o : Ordinal.{u_1}) :
(Ordinal.sup fun (n : ) => o * n) =
noncomputable def Acc.rank {α : Type u} {r : ααProp} {a : α} (h : Acc r a) :

The rank of an element a accessible under a relation r is defined inductively as the smallest ordinal greater than the ranks of all elements below it (i.e. elements b such that r b a).

Equations
Instances For
theorem Acc.rank_eq {α : Type u} {r : ααProp} {a : α} (h : Acc r a) :
h.rank = Ordinal.sup fun (b : { b : α // r b a }) => Order.succ .rank
theorem Acc.rank_lt_of_rel {α : Type u} {r : ααProp} {a : α} {b : α} (hb : Acc r b) (h : r a b) :
.rank < hb.rank

if r a b then the rank of a is less than the rank of b.

noncomputable def WellFounded.rank {α : Type u} {r : ααProp} (hwf : ) (a : α) :

The rank of an element a under a well-founded relation r is defined inductively as the smallest ordinal greater than the ranks of all elements below it (i.e. elements b such that r b a).

Equations
• hwf.rank a = .rank
Instances For
theorem WellFounded.rank_eq {α : Type u} {r : ααProp} {a : α} (hwf : ) :
hwf.rank a = Ordinal.sup fun (b : { b : α // r b a }) => Order.succ (hwf.rank b)
theorem WellFounded.rank_lt_of_rel {α : Type u} {r : ααProp} {a : α} {b : α} (hwf : ) (h : r a b) :
hwf.rank a < hwf.rank b
theorem WellFounded.rank_strictMono {α : Type u} [] [] :
StrictMono .rank
theorem WellFounded.rank_strictAnti {α : Type u} [] [] :
StrictAnti .rank