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 #

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.
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: the supremum of an indexed family of ordinals in Type u, as an ordinal in Type u.
bsup: the supremum 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.succ.lift = a.lift.succ

theorem ordinal.add_le_add_iff_left (a : ordinal) {b c : 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) :

@[simp]

theorem ordinal.card_succ (o : ordinal) :

o.succ.card = o.card + 1

theorem ordinal.nat_cast_succ (n : ℕ) :

↑n.succ = ↑(n.succ)

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.add_lt_add_iff_left (a : ordinal) {b c : ordinal} :

a + b < a + c ↔ b < c

theorem ordinal.lt_of_add_lt_add_right {a b c : ordinal} :

a + b < c + b → a < 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

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

theorem ordinal.type_ne_zero_iff_nonempty {α : Type u_1} {r : α → α → Prop} [is_well_order α r] :

ordinal.type r ≠ 0 ↔ nonempty α

@[simp]

theorem ordinal.type_eq_zero_iff_empty {α : Type u_1} {r : α → α → Prop} [is_well_order α r] :

ordinal.type r = 0 ↔ ¬nonempty α

@[protected]

theorem ordinal.one_ne_zero :

1 ≠ 0

@[protected, instance]

def ordinal.nontrivial :

nontrivial ordinal

theorem ordinal.zero_lt_one :

0 < 1

The predecessor of an ordinal #

def ordinal.pred (o : ordinal) :

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

Equations

o.pred = dite (∃ (a : ordinal), o = a.succ) (λ (h : ∃ (a : ordinal), o = a.succ), classical.some h) (λ (h : ¬∃ (a : ordinal), o = a.succ), o)

@[simp]

theorem ordinal.pred_succ (o : ordinal) :

o.succ.pred = o

theorem ordinal.pred_le_self (o : ordinal) :

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) :

o.pred.lift = o.lift.pred

Limit ordinals #

def ordinal.is_limit (o : ordinal) :

Prop

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

Equations

o.is_limit = (o ≠ 0 ∧ ∀ (a : ordinal), a < o → a.succ < o)

theorem ordinal.not_zero_is_limit :

theorem ordinal.not_succ_is_limit (o : ordinal) :

¬o.succ.is_limit

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 < o → x ≤ 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) :

o.lift.is_limit ↔ o.is_limit

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

def ordinal.limit_rec_on {C : ordinal → Sort u_2} (o : ordinal) (H₁ : C 0) (H₂ : Π (o : ordinal), C o → C o.succ) (H₃ : Π (o : ordinal), o.is_limit → (Π (o' : ordinal), o' < o → C 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

o.limit_rec_on H₁ H₂ H₃ = ordinal.wf.fix (λ (o : ordinal) (IH : Π (y : ordinal), y < o → C y), dite (o = 0) (λ (o0 : o = 0), _.mpr H₁) (λ (o0 : ¬o = 0), dite (∃ (a : ordinal), o = a.succ) (λ (h : ∃ (a : ordinal), o = a.succ), _.mpr (H₂ o.pred (IH o.pred _))) (λ (h : ¬∃ (a : ordinal), o = a.succ), H₃ o _ IH))) o

@[simp]

theorem ordinal.limit_rec_on_zero {C : ordinal → Sort u_2} (H₁ : C 0) (H₂ : Π (o : ordinal), C o → C o.succ) (H₃ : Π (o : ordinal), o.is_limit → (Π (o' : ordinal), o' < o → C o') → C o) :

0.limit_rec_on H₁ H₂ H₃ = H₁

@[simp]

theorem ordinal.limit_rec_on_succ {C : ordinal → Sort u_2} (o : ordinal) (H₁ : C 0) (H₂ : Π (o : ordinal), C o → C o.succ) (H₃ : Π (o : ordinal), o.is_limit → (Π (o' : ordinal), o' < o → C 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 : ordinal → Sort u_2} (o : ordinal) (H₁ : C 0) (H₂ : Π (o : ordinal), C o → C o.succ) (H₃ : Π (o : ordinal), o.is_limit → (Π (o' : ordinal), o' < o → C 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 : is_well_order α r] (h : (ordinal.type r).is_limit) (x : α) :

∃ (y : α), r x y

theorem ordinal.type_subrel_lt (o : ordinal) :

ordinal.type (subrel has_lt.lt {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 : ordinal → ordinal) :

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

ordinal.is_normal f = ((∀ (o : ordinal), f o < f o.succ) ∧ ∀ (o : ordinal), o.is_limit → ∀ (a : ordinal), f o ≤ a ↔ ∀ (b : ordinal), b < o → f b ≤ a)

theorem ordinal.is_normal.limit_le {f : ordinal → ordinal} (H : ordinal.is_normal f) {o : ordinal} :

o.is_limit → ∀ {a : ordinal}, f o ≤ a ↔ ∀ (b : ordinal), b < o → f b ≤ a

theorem ordinal.is_normal.limit_lt {f : ordinal → ordinal} (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 : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} :

f a < f b ↔ a < b

theorem ordinal.is_normal.le_iff {f : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} :

f a ≤ f b ↔ a ≤ b

theorem ordinal.is_normal.inj {f : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} :

f a = f b ↔ a = b

theorem ordinal.is_normal.le_self {f : ordinal → ordinal} (H : ordinal.is_normal f) (a : ordinal) :

a ≤ f a

theorem ordinal.is_normal.le_set {f : ordinal → ordinal} (H : ordinal.is_normal f) (p : ordinal → Prop) (p0 : ∃ (x : ordinal), p x) (S : ordinal) (H₂ : ∀ (o : ordinal), S ≤ o ↔ ∀ (a : ordinal), p a → a ≤ o) {o : ordinal} :

f S ≤ o ↔ ∀ (a : ordinal), p a → f a ≤ o

theorem ordinal.is_normal.le_set' {α : Type u_1} {f : ordinal → ordinal} (H : ordinal.is_normal f) (p : α → Prop) (g : α → ordinal) (p0 : ∃ (x : α), p x) (S : ordinal) (H₂ : ∀ (o : ordinal), S ≤ o ↔ ∀ (a : α), p a → g a ≤ o) {o : ordinal} :

f S ≤ o ↔ ∀ (a : α), p a → f (g a) ≤ o

theorem ordinal.is_normal.refl :

ordinal.is_normal id

theorem ordinal.is_normal.trans {f : ordinal → ordinal} {g : ordinal → ordinal} (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 : ordinal → ordinal} (H : ordinal.is_normal f) {o : ordinal} (l : o.is_limit) :

theorem ordinal.add_le_of_limit {a b c : ordinal} (h : b.is_limit) :

a + b ≤ c ↔ ∀ (b' : ordinal), b' < b → a + b' ≤ c

theorem ordinal.add_is_normal (a : ordinal) :

ordinal.is_normal (has_add.add a)

theorem ordinal.add_is_limit (a : ordinal) {b : ordinal} :

b.is_limit → (a + b).is_limit

Subtraction on ordinals #

def ordinal.sub (a b : ordinal) :

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

Equations

a.sub b = ordinal.omin {o : ordinal | a ≤ b + o} _

@[protected, instance]

def ordinal.has_sub :

has_sub ordinal

Equations

ordinal.has_sub = {sub := ordinal.sub}

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

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

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_omega :

@[simp]

theorem ordinal.one_add_of_omega_le {o : ordinal} (h : ω ≤ o) :

1 + o = o

Multiplication of ordinals #

@[protected, instance]

def ordinal.monoid :

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

Equations

ordinal.monoid = {mul := λ (a b : ordinal), quotient.lift_on₂ a b (λ (_x : Well_order), ordinal.monoid._match_2 _x) ordinal.monoid._proof_1, mul_assoc := ordinal.monoid._proof_2, one := 1, one_mul := ordinal.monoid._proof_3, mul_one := ordinal.monoid._proof_4, npow := npow_rec (mul_one_class.to_has_mul ordinal), npow_zero' := ordinal.monoid._proof_7, npow_succ' := ordinal.monoid._proof_8}
ordinal.monoid._match_2 {α := α, r := r, wo := wo} = λ (_x : Well_order), ordinal.monoid._match_1 α r wo _x
ordinal.monoid._match_1 α r wo {α := β, r := s, wo := wo'} = ⟦{α := β × α, r := prod.lex s r, wo := _}⟧

@[simp]

theorem ordinal.type_mul {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [is_well_order α r] [is_well_order β s] :

(ordinal.type r) * ordinal.type s = ordinal.type (prod.lex s r)

@[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 ≤ b → c * a ≤ c * b

theorem ordinal.mul_le_mul_right {a b : ordinal} (c : ordinal) :

a ≤ b → a * c ≤ b * c

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' < b → a * b' ≤ c

theorem ordinal.mul_is_normal {a : ordinal} (h : 0 < a) :

ordinal.is_normal (has_mul.mul 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 ≠ 0 → b ≠ 0 → a * 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]

def ordinal.div (a b : ordinal) :

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

Equations

a.div b = dite (b = 0) (λ (h : b = 0), 0) (λ (h : ¬b = 0), ordinal.omin {o : ordinal | a < b * o.succ} _)

@[protected, instance]

def ordinal.has_div :

has_div ordinal

Equations

ordinal.has_div = {div := ordinal.div}

@[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 / c → c * 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.is_limit_add_iff {a b : ordinal} :

(a + b).is_limit ↔ b.is_limit ∨ b = 0 ∧ a.is_limit

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 ∣ c → a ∣ 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 ≠ 0 → a ∣ b → a * (b / a) = b

theorem ordinal.le_of_dvd {a b : ordinal} :

b ≠ 0 → a ∣ b → a ≤ b

theorem ordinal.dvd_antisymm {a b : ordinal} (h₁ : a ∣ b) (h₂ : b ∣ a) :

a = b

@[protected, instance]

def ordinal.has_mod :

has_mod ordinal

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

Equations

ordinal.has_mod = {mod := λ (a b : ordinal), a - b * (a / b)}

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

Supremum of a family of ordinals #

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

The supremum of a family of ordinals

Equations

ordinal.sup f = ordinal.omin {c : ordinal | ∀ (i : ι), f i ≤ c} _

theorem ordinal.le_sup {ι : Type u_1} (f : ι → ordinal) (i : ι) :

f i ≤ ordinal.sup f

theorem ordinal.sup_le {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :

ordinal.sup f ≤ a ↔ ∀ (i : ι), f i ≤ a

theorem ordinal.lt_sup {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :

a < ordinal.sup f ↔ ∃ (i : ι), a < f i

theorem ordinal.is_normal.sup {f : ordinal → ordinal} (H : ordinal.is_normal f) {ι : Type u_1} {g : ι → ordinal} (h : nonempty ι) :

f (ordinal.sup g) = ordinal.sup (f ∘ g)

theorem ordinal.sup_ord {ι : Type u_1} (f : ι → cardinal) :

ordinal.sup (λ (i : ι), (f i).ord) = (cardinal.sup f).ord

theorem ordinal.sup_succ {ι : Type u_1} (f : ι → ordinal) :

ordinal.sup (λ (i : ι), (f i).succ) ≤ (ordinal.sup f).succ

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)) :

unbounded r (set.range f)

def ordinal.bsup (o : ordinal) :

(Π (a : ordinal), a < o → ordinal) → 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

o.bsup = ordinal.bsup._match_1 o (quotient.out o) _
ordinal.bsup._match_1 ⟦{α := α, r := r, wo := _x}⟧ {α := α, r := r, wo := _x} rfl f = ordinal.sup (λ (a : α), f (ordinal.typein r a) _)

theorem ordinal.bsup_le {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {a : ordinal} :

o.bsup f ≤ a ↔ ∀ (i : ordinal) (h : i < o), f i h ≤ a

theorem ordinal.bsup_type {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (f : Π (a : ordinal), a < ordinal.type r → ordinal) :

(ordinal.type r).bsup f = ordinal.sup (λ (a : α), f (ordinal.typein r a) _)

theorem ordinal.le_bsup {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) (i : ordinal) (h : i < o) :

f i h ≤ o.bsup f

theorem ordinal.lt_bsup {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} (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 {f : ordinal → ordinal} (H : ordinal.is_normal f) {o : ordinal} (g : Π (a : ordinal), a < o → ordinal) (h : o ≠ 0) :

f (o.bsup g) = o.bsup (λ (a : ordinal) (h : a < o), f (g a h))

theorem ordinal.is_normal.bsup_eq {f : ordinal → ordinal} (H : ordinal.is_normal f) {o : ordinal} (h : o.is_limit) :

o.bsup (λ (x : ordinal) (_x : x < o), f x) = f o

Ordinal exponential #

def ordinal.power (a b : ordinal) :

The ordinal exponential, defined by transfinite recursion.

Equations

a.power b = ite (a = 0) (1 - b) (b.limit_rec_on 1 (λ (_x IH : ordinal), IH * a) (λ (b : ordinal) (_x : b.is_limit), b.bsup))

@[protected, instance]

def ordinal.has_pow :

has_pow ordinal ordinal

Equations

ordinal.has_pow = {pow := ordinal.power}

theorem ordinal.zero_power' (a : ordinal) :

0 ^ a = 1 - a

@[simp]

theorem ordinal.zero_power {a : ordinal} (a0 : a ≠ 0) :

0 ^ a = 0

@[simp]

theorem ordinal.power_zero (a : ordinal) :

a ^ 0 = 1

@[simp]

theorem ordinal.power_succ (a b : ordinal) :

a ^ b.succ = (a ^ b) * a

theorem ordinal.power_limit {a b : ordinal} (a0 : a ≠ 0) (h : b.is_limit) :

a ^ b = b.bsup (λ (c : ordinal) (_x : c < b), a ^ c)

theorem ordinal.power_le_of_limit {a b c : ordinal} (a0 : a ≠ 0) (h : b.is_limit) :

a ^ b ≤ c ↔ ∀ (b' : ordinal), b' < b → a ^ b' ≤ c

theorem ordinal.lt_power_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.power_one (a : ordinal) :

a ^ 1 = a

@[simp]

theorem ordinal.one_power (a : ordinal) :

1 ^ a = 1

theorem ordinal.power_pos {a : ordinal} (b : ordinal) (a0 : 0 < a) :

0 < a ^ b

theorem ordinal.power_ne_zero {a : ordinal} (b : ordinal) (a0 : a ≠ 0) :

a ^ b ≠ 0

theorem ordinal.power_is_normal {a : ordinal} (h : 1 < a) :

ordinal.is_normal (λ (_y : ordinal), a ^ _y)

theorem ordinal.power_lt_power_iff_right {a b c : ordinal} (a1 : 1 < a) :

a ^ b < a ^ c ↔ b < c

theorem ordinal.power_le_power_iff_right {a b c : ordinal} (a1 : 1 < a) :

a ^ b ≤ a ^ c ↔ b ≤ c

theorem ordinal.power_right_inj {a b c : ordinal} (a1 : 1 < a) :

a ^ b = a ^ c ↔ b = c

theorem ordinal.power_is_limit {a b : ordinal} (a1 : 1 < a) :

b.is_limit → (a ^ b).is_limit

theorem ordinal.power_is_limit_left {a b : ordinal} (l : a.is_limit) (hb : b ≠ 0) :

(a ^ b).is_limit

theorem ordinal.power_le_power_right {a b c : ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) :

a ^ b ≤ a ^ c

theorem ordinal.power_le_power_left {a b : ordinal} (c : ordinal) (ab : a ≤ b) :

a ^ c ≤ b ^ c

theorem ordinal.le_power_self {a : ordinal} (b : ordinal) (a1 : 1 < a) :

b ≤ a ^ b

theorem ordinal.power_lt_power_left_of_succ {a b c : ordinal} (ab : a < b) :

a ^ c.succ < b ^ c.succ

theorem ordinal.power_add (a b c : ordinal) :

a ^ (b + c) = (a ^ b) * a ^ c

theorem ordinal.power_dvd_power (a : ordinal) {b c : ordinal} (h : b ≤ c) :

a ^ b ∣ a ^ c

theorem ordinal.power_dvd_power_iff {a b c : ordinal} (a1 : 1 < a) :

a ^ b ∣ a ^ c ↔ b ≤ c

theorem ordinal.power_mul (a b c : ordinal) :

a ^ b * c = (a ^ b) ^ c

Ordinal logarithm #

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.

Equations

b.log x = dite (1 < b) (λ (h : 1 < b), (ordinal.omin {o : ordinal | x < b ^ o} _).pred) (λ (h : ¬1 < b), 0)

@[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_power_succ_log {b : ordinal} (b1 : 1 < b) (x : ordinal) :

x < b ^ (b.log x).succ

theorem ordinal.power_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

The Cantor normal form #

theorem ordinal.CNF_aux {b o : ordinal} (b0 : b ≠ 0) (o0 : o ≠ 0) :

o % b ^ b.log o < o

def ordinal.CNF_rec {b : ordinal} (b0 : b ≠ 0) {C : ordinal → Sort u_2} (H0 : C 0) (H : Π (o : ordinal), o ≠ 0 → o % b ^ b.log o < o → C (o % b ^ b.log o) → C o) (o : ordinal) :

C o

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

Equations

ordinal.CNF_rec b0 H0 H o = dite (o = 0) (λ (o0 : o = 0), _.mpr H0) (λ (o0 : ¬o = 0), have this : o % b ^ b.log o < o, from _, H o o0 this (ordinal.CNF_rec b0 H0 H (o % b ^ b.log o)))

@[simp]

theorem ordinal.CNF_rec_zero {b : ordinal} (b0 : b ≠ 0) {C : ordinal → Sort u_2} {H0 : C 0} {H : Π (o : ordinal), o ≠ 0 → o % b ^ b.log o < o → C (o % b ^ b.log o) → C o} :

ordinal.CNF_rec b0 H0 H 0 = H0

@[simp]

theorem ordinal.CNF_rec_ne_zero {b : ordinal} (b0 : b ≠ 0) {C : ordinal → Sort u_2} {H0 : C 0} {H : Π (o : ordinal), o ≠ 0 → o % b ^ b.log o < o → C (o % b ^ b.log o) → C o} {o : ordinal} (o0 : o ≠ 0) :

ordinal.CNF_rec b0 H0 H o = H o o0 _ (ordinal.CNF_rec b0 H0 H (o % b ^ b.log o))

def ordinal.CNF (b : ordinal := ω) (o : ordinal) :

list (ordinal × 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

ordinal.CNF b o = dite (b = 0) (λ (b0 : b = 0), list.nil) (λ (b0 : ¬b = 0), ordinal.CNF_rec b0 list.nil (λ (o : ordinal) (o0 : o ≠ 0) (h : o % b ^ ordinal.log b o < o) (IH : list (ordinal × ordinal)), (ordinal.log b o, o / b ^ ordinal.log b o) :: IH) o)

@[simp]

theorem ordinal.zero_CNF (o : ordinal) :

ordinal.CNF 0 o = list.nil

@[simp]

theorem ordinal.CNF_zero (b : ordinal := ω) :

ordinal.CNF b 0 = list.nil

theorem ordinal.CNF_ne_zero {b o : ordinal} (b0 : b ≠ 0) (o0 : o ≠ 0) :

ordinal.CNF b o = (b.log o, o / b ^ b.log o) :: ordinal.CNF b (o % b ^ b.log o)

theorem ordinal.one_CNF {o : ordinal} (o0 : o ≠ 0) :

ordinal.CNF 1 o = [(0, o)]

theorem ordinal.CNF_foldr {b : ordinal} (b0 : b ≠ 0) (o : ordinal) :

list.foldr (λ (p : ordinal × ordinal) (r : ordinal), (b ^ p.fst) * p.snd + r) 0 (ordinal.CNF b o) = o

theorem ordinal.CNF_pairwise_aux (b : ordinal := ω) (o : ordinal) :

(∀ (p : ordinal × ordinal), p ∈ ordinal.CNF b o → p.fst ≤ ordinal.log b o) ∧ list.pairwise (λ (p q : ordinal × ordinal), q.fst < p.fst) (ordinal.CNF b o)

theorem ordinal.CNF_pairwise (b : ordinal := ω) (o : ordinal) :

list.pairwise (λ (p q : ordinal × ordinal), q.fst < p.fst) (ordinal.CNF b o)

theorem ordinal.CNF_fst_le_log (b : ordinal := ω) (o : ordinal) (p : ordinal × ordinal) (H : p ∈ ordinal.CNF b o) :

p.fst ≤ ordinal.log b o

theorem ordinal.CNF_fst_le (b : ordinal := ω) (o : ordinal) (p : ordinal × ordinal) (H : p ∈ ordinal.CNF b o) :

theorem ordinal.CNF_snd_lt {b : ordinal} (b1 : 1 < b) (o : ordinal) (p : ordinal × ordinal) (H : p ∈ ordinal.CNF b o) :

p.snd < b

theorem ordinal.CNF_sorted (b : ordinal := ω) (o : ordinal) :

list.sorted gt (list.map prod.fst (ordinal.CNF b 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_power {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 : ℕ} :

↑n ≤ o.card ↔ ↑n ≤ o

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

o.card ≤ ↑n ↔ o ≤ ↑n

@[simp]

theorem ordinal.card_eq_nat {o : ordinal} {n : ℕ} :

o.card = ↑n ↔ o = ↑n

@[simp]

theorem ordinal.type_fin (n : ℕ) :

ordinal.type has_lt.lt = ↑n

@[simp]

theorem ordinal.lift_nat_cast (n : ℕ) :

↑n.lift = ↑n

theorem ordinal.lift_type_fin (n : ℕ) :

(ordinal.type has_lt.lt).lift = ↑n

theorem ordinal.fintype_card {α : Type u_1} (r : α → α → Prop) [is_well_order α r] [fintype α] :

ordinal.type r = ↑(fintype.card α)

Properties of `omega` #

@[simp]

theorem cardinal.ord_omega :

cardinal.omega.ord = ω

@[simp]

theorem cardinal.add_one_of_omega_le {c : cardinal} (h : cardinal.omega ≤ 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_ne_zero :

theorem ordinal.one_lt_omega :

1 < ω

theorem ordinal.omega_is_limit :

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.omega_le_of_is_limit {o : ordinal} (h : o.is_limit) :

theorem ordinal.add_omega {a : ordinal} (h : 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.is_limit_iff_omega_dvd {a : ordinal} :

a.is_limit ↔ a ≠ 0 ∧ ω ∣ a

theorem ordinal.power_lt_omega {a b : ordinal} (ha : a < ω) (hb : b < ω) :

a ^ b < ω

theorem ordinal.add_omega_power {a b : ordinal} (h : a < ω ^ b) :

a + ω ^ b = ω ^ b

theorem ordinal.add_lt_omega_power {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 < o → a + 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 < ω) :

theorem ordinal.mul_lt_omega_power {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} :

ω ∣ b → a * b = b

theorem ordinal.mul_omega_power_power {a b : ordinal} (a0 : 0 < a) (h : a < ω ^ ω ^ b) :

a * ω ^ ω ^ b = ω ^ ω ^ b

theorem ordinal.power_omega {a : ordinal} (a1 : 1 < a) (h : a < ω) :

Fixed points of normal functions #

def ordinal.nfp (f : ordinal → ordinal) (a : ordinal) :

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

Equations

ordinal.nfp f a = ordinal.sup (λ (n : ℕ), f^[n] a)

theorem ordinal.iterate_le_nfp (f : ordinal → ordinal) (a : ordinal) (n : ℕ) :

f^[n] a ≤ ordinal.nfp f a

theorem ordinal.le_nfp_self (f : ordinal → ordinal) (a : ordinal) :

a ≤ ordinal.nfp f a

theorem ordinal.is_normal.lt_nfp {f : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} :

f b < ordinal.nfp f a ↔ b < ordinal.nfp f a

theorem ordinal.is_normal.nfp_le {f : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} :

ordinal.nfp f a ≤ f b ↔ ordinal.nfp f a ≤ b

theorem ordinal.is_normal.nfp_le_fp {f : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} (ab : a ≤ b) (h : f b ≤ b) :

ordinal.nfp f a ≤ b

theorem ordinal.is_normal.nfp_fp {f : ordinal → ordinal} (H : ordinal.is_normal f) (a : ordinal) :

f (ordinal.nfp f a) = ordinal.nfp f a

theorem ordinal.is_normal.le_nfp {f : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} :

f b ≤ ordinal.nfp f a ↔ b ≤ ordinal.nfp f a

theorem ordinal.nfp_eq_self {f : ordinal → ordinal} {a : ordinal} (h : f a = a) :

ordinal.nfp f a = a

def ordinal.deriv (f : ordinal → ordinal) (o : ordinal) :

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

Equations

ordinal.deriv f o = o.limit_rec_on (ordinal.nfp f 0) (λ (a IH : ordinal), ordinal.nfp f IH.succ) (λ (a : ordinal) (l : a.is_limit), a.bsup)

@[simp]

theorem ordinal.deriv_zero (f : ordinal → ordinal) :

ordinal.deriv f 0 = ordinal.nfp f 0

@[simp]

theorem ordinal.deriv_succ (f : ordinal → ordinal) (o : ordinal) :

ordinal.deriv f o.succ = ordinal.nfp f (ordinal.deriv f o).succ

theorem ordinal.deriv_limit (f : ordinal → ordinal) {o : ordinal} :

o.is_limit → ordinal.deriv f o = o.bsup (λ (a : ordinal) (_x : a < o), ordinal.deriv f a)

theorem ordinal.deriv_is_normal (f : ordinal → ordinal) :

ordinal.is_normal (ordinal.deriv f)

theorem ordinal.is_normal.deriv_fp {f : ordinal → ordinal} (H : ordinal.is_normal f) (o : ordinal) :

f (ordinal.deriv f o) = ordinal.deriv f o

theorem ordinal.is_normal.fp_iff_deriv {f : ordinal → ordinal} (H : ordinal.is_normal f) {a : ordinal} :

f a ≤ a ↔ ∃ (o : ordinal), a = ordinal.deriv f o