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

source
@[simp]
theorem ordinal.lift_add (a b : ordinal) :
(a + b).lift = a.lift + b.lift
source
@[simp]
theorem ordinal.lift_succ (a : ordinal) :
a.succ.lift = a.lift.succ
source
@[protected, instance]
def ordinal.has_le.le.add_contravariant_class  :
contravariant_class ordinal ordinal has_add.add has_le.le
source
theorem ordinal.add_succ (o₁ o₂ : ordinal) :
o₁ + o₂.succ = (o₁ + o₂).succ
source
@[simp]
theorem ordinal.succ_zero  :
0.succ = 1
source
theorem ordinal.one_le_iff_pos {o : ordinal} :
1 ≤ o ↔ 0 < o
source
theorem ordinal.one_le_iff_ne_zero {o : ordinal} :
1 ≤ o ↔ o ≠ 0
source
theorem ordinal.succ_pos (o : ordinal) :
0 < o.succ
source
theorem ordinal.succ_ne_zero (o : ordinal) :
o.succ ≠ 0
source
@[simp]
theorem ordinal.card_succ (o : ordinal) :
o.succ.card = o.card + 1
source
theorem ordinal.nat_cast_succ (n : ℕ) :
↑n.succ = ↑(n.succ)
source
theorem ordinal.add_left_cancel (a : ordinal) {b c : ordinal} :
a + b = a + c ↔ b = c
source
theorem ordinal.lt_one_iff_zero {a : ordinal} :
a < 1 ↔ a = 0
source
@[protected, instance]
def ordinal.has_lt.lt.covariant_class  :
covariant_class ordinal ordinal has_add.add has_lt.lt
source
@[protected, instance]
def ordinal.has_lt.lt.contravariant_class  :
contravariant_class ordinal ordinal has_add.add has_lt.lt
source
theorem ordinal.lt_of_add_lt_add_right {a b c : ordinal} :
a + b < c + b → a < c
source
@[simp]
theorem ordinal.succ_lt_succ {a b : ordinal} :
a.succ < b.succ ↔ a < b
source
@[simp]
theorem ordinal.succ_le_succ {a b : ordinal} :
a.succ ≤ b.succ ↔ a ≤ b
source
theorem ordinal.succ_inj {a b : ordinal} :
a.succ = b.succ ↔ a = b
source
theorem ordinal.add_le_add_iff_right {a b : ordinal} (n : ℕ) :
a + ↑n ≤ b + ↑n ↔ a ≤ b
source
theorem ordinal.add_right_cancel {a b : ordinal} (n : ℕ) :
a + ↑n = b + ↑n ↔ a = b

The zero ordinal #

source
@[simp]
theorem ordinal.card_eq_zero {o : ordinal} :
o.card = 0 ↔ o = 0
source
@[simp]
theorem ordinal.type_eq_zero_of_empty {α : Type u_1} {r : α → α → Prop} [is_well_order α r] [is_empty α] :
ordinal.type r = 0
source
@[simp]
theorem ordinal.type_eq_zero_iff_is_empty {α : Type u_1} {r : α → α → Prop} [is_well_order α r] :
ordinal.type r = 0 ↔ is_empty α
source
theorem ordinal.type_ne_zero_iff_nonempty {α : Type u_1} {r : α → α → Prop} [is_well_order α r] :
ordinal.type r ≠ 0 ↔ nonempty α
source
@[protected]
theorem ordinal.one_ne_zero  :
1 ≠ 0
source
@[protected, instance]
def ordinal.nontrivial  :
nontrivial ordinal
source
@[protected, instance]
def ordinal.α.nonempty  :
nonempty (quotient.out 1).α
source
theorem ordinal.zero_lt_one  :
0 < 1
source
theorem ordinal.le_one_iff {a : ordinal} :
a ≤ 1 ↔ a = 0 ∨ a = 1
source
theorem ordinal.add_eq_zero_iff {a b : ordinal} :
a + b = 0 ↔ a = 0 ∧ b = 0
source
theorem ordinal.left_eq_zero_of_add_eq_zero {a b : ordinal} (h : a + b = 0) :
a = 0
source
theorem ordinal.right_eq_zero_of_add_eq_zero {a b : ordinal} (h : a + b = 0) :
b = 0

The predecessor of an ordinal #

source
noncomputable def ordinal.pred (o : ordinal) :
ordinal

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

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

Limit ordinals #

source
def ordinal.is_limit (o : ordinal) :
Prop

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

Equations
source
theorem ordinal.not_zero_is_limit  :
¬0.is_limit
source
theorem ordinal.not_succ_is_limit (o : ordinal) :
¬o.succ.is_limit
source
theorem ordinal.not_succ_of_is_limit {o : ordinal} (h : o.is_limit) :
¬∃ (a : ordinal), o = a.succ
source
theorem ordinal.succ_lt_of_is_limit {o : ordinal} (h : o.is_limit) {a : ordinal} :
a.succ < o ↔ a < o
source
theorem ordinal.le_succ_of_is_limit {o : ordinal} (h : o.is_limit) {a : ordinal} :
o ≤ a.succ ↔ o ≤ a
source
theorem ordinal.limit_le {o : ordinal} (h : o.is_limit) {a : ordinal} :
o ≤ a ↔ ∀ (x : ordinal), x < o → x ≤ a
source
theorem ordinal.lt_limit {o : ordinal} (h : o.is_limit) {a : ordinal} :
a < o ↔ ∃ (x : ordinal) (H : x < o), a < x
source
@[simp]
theorem ordinal.lift_is_limit (o : ordinal) :
o.lift.is_limit ↔ o.is_limit
source
theorem ordinal.is_limit.pos {o : ordinal} (h : o.is_limit) :
0 < o
source
theorem ordinal.is_limit.one_lt {o : ordinal} (h : o.is_limit) :
1 < o
source
theorem ordinal.is_limit.nat_lt {o : ordinal} (h : o.is_limit) (n : ℕ) :
↑n < o
source
theorem ordinal.zero_or_succ_or_limit (o : ordinal) :
o = 0 ∨ (∃ (a : ordinal), o = a.succ) ∨ o.is_limit
source
noncomputable 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
source
@[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₁
source
@[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₃)
source
@[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₃)
source
@[protected, instance]
noncomputable def ordinal.α.order_top (o : ordinal) :
order_top (quotient.out o.succ).α
Equations
source
theorem ordinal.enum_succ_eq_top {o : ordinal} :
ordinal.enum has_lt.lt o _ = ⊤
source
theorem ordinal.has_succ_of_type_succ_lt {α : Type u_1} {r : α → α → Prop} [wo : is_well_order α r] (h : ∀ (a : ordinal), a < ordinal.type r → a.succ < ordinal.type r) (x : α) :
∃ (y : α), r x y
source
theorem ordinal.out_no_max_of_succ_lt {o : ordinal} (ho : ∀ (a : ordinal), a < o → a.succ < o) :
no_max_order (quotient.out o).α
source
theorem ordinal.type_subrel_lt (o : ordinal) :
ordinal.type (subrel has_lt.lt {o' : ordinal | o' < o}) = o.lift
source
theorem ordinal.mk_initial_seg (o : ordinal) :
# ↥{o' : ordinal | o' < o} = o.card.lift

Normal ordinal functions #

source
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
source
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
source
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
source
theorem ordinal.is_normal.strict_mono {f : ordinal → ordinal} (H : ordinal.is_normal f) :
strict_mono f
source
theorem ordinal.is_normal.monotone {f : ordinal → ordinal} (H : ordinal.is_normal f) :
monotone f
source
theorem ordinal.is_normal_iff_strict_mono_limit (f : ordinal → ordinal) :
ordinal.is_normal f ↔ strict_mono f ∧ ∀ (o : ordinal), o.is_limit → ∀ (a : ordinal), (∀ (b : ordinal), b < o → f b ≤ a) → f o ≤ a
source
theorem ordinal.is_normal.lt_iff {f : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} :
f a < f b ↔ a < b
source
theorem ordinal.is_normal.le_iff {f : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} :
f a ≤ f b ↔ a ≤ b
source
theorem ordinal.is_normal.inj {f : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} :
f a = f b ↔ a = b
source
theorem ordinal.is_normal.self_le {f : ordinal → ordinal} (H : ordinal.is_normal f) (a : ordinal) :
a ≤ f a
source
theorem ordinal.is_normal.le_set {f : ordinal → ordinal} (H : ordinal.is_normal f) (p : set ordinal) (p0 : p.nonempty) (b : ordinal) (H₂ : ∀ (o : ordinal), b ≤ o ↔ ∀ (a : ordinal), a ∈ p → a ≤ o) {o : ordinal} :
f b ≤ o ↔ ∀ (a : ordinal), a ∈ p → f a ≤ o
source
theorem ordinal.is_normal.le_set' {α : Type u_1} {f : ordinal → ordinal} (H : ordinal.is_normal f) (p : set α) (g : α → ordinal) (p0 : p.nonempty) (b : ordinal) (H₂ : ∀ (o : ordinal), b ≤ o ↔ ∀ (a : α), a ∈ p → g a ≤ o) {o : ordinal} :
f b ≤ o ↔ ∀ (a : α), a ∈ p → f (g a) ≤ o
source
theorem ordinal.is_normal.refl  :
ordinal.is_normal id
source
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))
source
theorem ordinal.is_normal.is_limit {f : ordinal → ordinal} (H : ordinal.is_normal f) {o : ordinal} (l : o.is_limit) :
(f o).is_limit
source
theorem ordinal.is_normal.le_iff_eq {f : ordinal → ordinal} (H : ordinal.is_normal f) {a : ordinal} :
f a ≤ a ↔ f a = a
source
theorem ordinal.add_le_of_limit {a b c : ordinal} (h : b.is_limit) :
a + b ≤ c ↔ ∀ (b' : ordinal), b' < b → a + b' ≤ c
source
theorem ordinal.add_is_normal (a : ordinal) :
ordinal.is_normal (has_add.add a)
source
theorem ordinal.add_is_limit (a : ordinal) {b : ordinal} :
b.is_limit → (a + b).is_limit

Subtraction on ordinals #

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

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

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

The set in the definition of subtraction is nonempty.

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

Multiplication of ordinals #

source
@[protected, instance]
def ordinal.monoid  :
monoid ordinal

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

Equations
source
@[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)
source
@[simp]
theorem ordinal.lift_mul (a b : ordinal) :
(a * b).lift = (a.lift) * b.lift
source
@[simp]
theorem ordinal.card_mul (a b : ordinal) :
(a * b).card = (a.card) * b.card
source
theorem ordinal.mul_eq_zero_iff {a b : ordinal} :
a * b = 0 ↔ a = 0 ∨ b = 0
source
@[simp]
theorem ordinal.mul_zero (a : ordinal) :
a * 0 = 0
source
@[simp]
theorem ordinal.zero_mul (a : ordinal) :
0 * a = 0
source
theorem ordinal.mul_add (a b c : ordinal) :
a * (b + c) = a * b + a * c
source
@[simp]
theorem ordinal.mul_add_one (a b : ordinal) :
a * (b + 1) = a * b + a
source
@[simp]
theorem ordinal.mul_one_add (a b : ordinal) :
a * (1 + b) = a + a * b
source
@[simp]
theorem ordinal.mul_succ (a b : ordinal) :
a * b.succ = a * b + a
source
theorem ordinal.mul_two (a : ordinal) :
a * 2 = a + a
source
@[protected, instance]
def ordinal.has_le.le.mul_covariant_class  :
covariant_class ordinal ordinal has_mul.mul has_le.le
source
@[protected, instance]
def ordinal.has_le.le.mul_swap_covariant_class  :
covariant_class ordinal ordinal (function.swap has_mul.mul) has_le.le
source
theorem ordinal.le_mul_left (a : ordinal) {b : ordinal} (hb : 0 < b) :
a ≤ a * b
source
theorem ordinal.le_mul_right (a : ordinal) {b : ordinal} (hb : 0 < b) :
a ≤ b * a
source
theorem ordinal.mul_le_of_limit {a b c : ordinal} (h : b.is_limit) :
a * b ≤ c ↔ ∀ (b' : ordinal), b' < b → a * b' ≤ c
source
theorem ordinal.mul_is_normal {a : ordinal} (h : 0 < a) :
ordinal.is_normal (has_mul.mul a)
source
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'
source
theorem ordinal.mul_lt_mul_iff_left {a b c : ordinal} (a0 : 0 < a) :
a * b < a * c ↔ b < c
source
theorem ordinal.mul_le_mul_iff_left {a b c : ordinal} (a0 : 0 < a) :
a * b ≤ a * c ↔ b ≤ c
source
theorem ordinal.mul_lt_mul_of_pos_left {a b c : ordinal} (h : a < b) (c0 : 0 < c) :
c * a < c * b
source
theorem ordinal.mul_pos {a b : ordinal} (h₁ : 0 < a) (h₂ : 0 < b) :
0 < a * b
source
theorem ordinal.mul_ne_zero {a b : ordinal} :
a ≠ 0 → b ≠ 0 → a * b ≠ 0
source
theorem ordinal.le_of_mul_le_mul_left {a b c : ordinal} (h : c * a ≤ c * b) (h0 : 0 < c) :
a ≤ b
source
theorem ordinal.mul_right_inj {a b c : ordinal} (a0 : 0 < a) :
a * b = a * c ↔ b = c
source
theorem ordinal.mul_is_limit {a b : ordinal} (a0 : 0 < a) :
b.is_limit → (a * b).is_limit
source
theorem ordinal.mul_is_limit_left {a b : ordinal} (l : a.is_limit) (b0 : 0 < b) :
(a * b).is_limit
source
theorem ordinal.smul_eq_mul (n : ℕ) (a : ordinal) :
n • a = a * ↑n

Division on ordinals #

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

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

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

The set in the definition of division is nonempty.

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

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

Equations
source
theorem ordinal.mod_def (a b : ordinal) :
a % b = a - b * (a / b)
source
@[simp]
theorem ordinal.mod_zero (a : ordinal) :
a % 0 = a
source
theorem ordinal.mod_eq_of_lt {a b : ordinal} (h : a < b) :
a % b = a
source
@[simp]
theorem ordinal.zero_mod (b : ordinal) :
0 % b = 0
source
theorem ordinal.div_add_mod (a b : ordinal) :
b * (a / b) + a % b = a
source
theorem ordinal.mod_lt (a : ordinal) {b : ordinal} (h : b ≠ 0) :
a % b < b
source
@[simp]
theorem ordinal.mod_self (a : ordinal) :
a % a = 0
source
@[simp]
theorem ordinal.mod_one (a : ordinal) :
a % 1 = 0
source
theorem ordinal.dvd_of_mod_eq_zero {a b : ordinal} (H : a % b = 0) :
b ∣ a
source
theorem ordinal.mod_eq_zero_of_dvd {a b : ordinal} (H : b ∣ a) :
a % b = 0
source
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.

source
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
source
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
source
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
source
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
source
@[simp]
theorem ordinal.bfamily_of_family'_typein {α : Type u_1} {ι : Type u_2} (r : ι → ι → Prop) [is_well_order ι r] (f : ι → α) (i : ι) :
ordinal.bfamily_of_family' r f (ordinal.typein r i) _ = f i
source
@[simp]
theorem ordinal.bfamily_of_family_typein {α : Type u_1} {ι : Type u_2} (f : ι → α) (i : ι) :
ordinal.bfamily_of_family f (ordinal.typein well_ordering_rel i) _ = f i
source
@[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) :
ordinal.family_of_bfamily' r ho f (ordinal.enum r i _) = f i hi
source
@[simp]
theorem ordinal.family_of_bfamily_enum {α : Type u_1} (o : ordinal) (f : Π (a : ordinal), a < o → α) (i : ordinal) (hi : i < o) :
o.family_of_bfamily f (ordinal.enum has_lt.lt i _) = f i hi
source
def ordinal.brange {α : Type u_1} (o : ordinal) (f : Π (a : ordinal), a < o → α) :
set α

The range of a family indexed by ordinals.

Equations
source
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
source
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
source
@[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 → α) :
set.range (ordinal.family_of_bfamily' r ho f) = o.brange f
source
@[simp]
theorem ordinal.range_family_of_bfamily {α : Type u_1} {o : ordinal} (f : Π (a : ordinal), a < o → α) :
set.range (o.family_of_bfamily f) = o.brange f
source
@[simp]
theorem ordinal.brange_bfamily_of_family' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [is_well_order ι r] (f : ι → α) :
(ordinal.type r).brange (ordinal.bfamily_of_family' r f) = set.range f
source
@[simp]
theorem ordinal.brange_bfamily_of_family {α : Type u_1} {ι : Type u} (f : ι → α) :
(ordinal.type well_ordering_rel).brange (ordinal.bfamily_of_family f) = set.range f
source
@[simp]
theorem ordinal.brange_const {α : Type u_1} {o : ordinal} (ho : o ≠ 0) {c : α} :
o.brange (λ (_x : ordinal) (_x : _x < o), c) = {c}
source
theorem ordinal.comp_bfamily_of_family' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [is_well_order ι r] (f : ι → α) (g : α → β) :
(λ (i : ordinal) (hi : i < ordinal.type r), g (ordinal.bfamily_of_family' r f i hi)) = ordinal.bfamily_of_family' r (g ∘ f)
source
theorem ordinal.comp_bfamily_of_family {α : Type u_1} {β : Type u_2} {ι : Type u} (f : ι → α) (g : α → β) :
(λ (i : ordinal) (hi : i < ordinal.type well_ordering_rel), g (ordinal.bfamily_of_family f i hi)) = ordinal.bfamily_of_family (g ∘ f)
source
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))
source
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 #

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

The supremum of a family of ordinals

Equations
source
@[simp]
theorem ordinal.Sup_eq_sup {ι : Type u} (f : ι → ordinal) :
Sup (set.range f) = ordinal.sup f
source
theorem ordinal.bdd_above_range {ι : Type u} (f : ι → ordinal) :
bdd_above (set.range f)

The range of any family of ordinals is bounded above. See also lsub_not_mem_range.

source
theorem ordinal.le_sup {ι : Type u_1} (f : ι → ordinal) (i : ι) :
f i ≤ ordinal.sup f
source
theorem ordinal.sup_le_iff {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
ordinal.sup f ≤ a ↔ ∀ (i : ι), f i ≤ a
source
theorem ordinal.sup_le {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
(∀ (i : ι), f i ≤ a) → ordinal.sup f ≤ a
source
theorem ordinal.lt_sup {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
a < ordinal.sup f ↔ ∃ (i : ι), a < f i
source
theorem ordinal.ne_sup_iff_lt_sup {ι : Type u_1} {f : ι → ordinal} :
(∀ (i : ι), f i ≠ ordinal.sup f) ↔ ∀ (i : ι), f i < ordinal.sup f
source
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) :
a.succ < ordinal.sup f
source
@[simp]
theorem ordinal.sup_eq_zero_iff {ι : Type u_1} {f : ι → ordinal} :
ordinal.sup f = 0 ↔ ∀ (i : ι), f i = 0
source
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)
source
theorem ordinal.sup_empty {ι : Type u_1} [is_empty ι] (f : ι → ordinal) :
ordinal.sup f = 0
source
theorem ordinal.sup_ord {ι : Type u_1} (f : ι → cardinal) :
ordinal.sup (λ (i : ι), (f i).ord) = (cardinal.sup f).ord
source
theorem ordinal.sup_const {ι : Type u_1} [hι : nonempty ι] (o : ordinal) :
ordinal.sup (λ (_x : ι), o) = o
source
theorem ordinal.sup_le_of_range_subset {ι : Type u} {ι' : Type v} {f : ι → ordinal} {g : ι' → ordinal} (h : set.range f ⊆ set.range g) :
ordinal.sup f ≤ ordinal.sup g
source
theorem ordinal.sup_eq_of_range_eq {ι : Type u} {ι' : Type v} {f : ι → ordinal} {g : ι' → ordinal} (h : set.range f = set.range g) :
ordinal.sup f = ordinal.sup g
source
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)) :
set.unbounded r (set.range f)
source
theorem ordinal.le_sup_shrink_equiv {s : set ordinal} (hs : small ↥s) (a : ordinal) (ha : a ∈ s) :
a ≤ ordinal.sup (λ (x : shrink ↥s), (⇑((equiv_shrink ↥s).symm) x).val)
source
theorem ordinal.small_Iio (o : ordinal) :
small ↥(set.Iio o)
source
theorem ordinal.bdd_above_iff_small {s : set ordinal} :
bdd_above s ↔ small ↥s
source
theorem ordinal.sup_eq_Sup {s : set ordinal} (hs : small ↥s) :
ordinal.sup (λ (x : shrink ↥s), ↑(⇑((equiv_shrink ↥s).symm) x)) = Sup s
source
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 < o → ordinal) :
ordinal.sup (ordinal.family_of_bfamily' r ho f) = ordinal.sup (ordinal.family_of_bfamily' r' ho' f)
source
noncomputable def ordinal.bsup (o : ordinal) (f : Π (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 a special case of sup over the family provided by family_of_bfamily.

Equations
source
@[simp]
theorem ordinal.sup_eq_bsup {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
ordinal.sup (o.family_of_bfamily f) = o.bsup f
source
@[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 < o → ordinal) :
ordinal.sup (ordinal.family_of_bfamily' r ho f) = o.bsup f
source
@[simp]
theorem ordinal.Sup_eq_bsup {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
Sup (o.brange f) = o.bsup f
source
@[simp]
theorem ordinal.bsup_eq_sup' {ι : Type u_1} (r : ι → ι → Prop) [is_well_order ι r] (f : ι → ordinal) :
(ordinal.type r).bsup (ordinal.bfamily_of_family' r f) = ordinal.sup f
source
theorem ordinal.bsup_eq_bsup {ι : Type u} (r r' : ι → ι → Prop) [is_well_order ι r] [is_well_order ι r'] (f : ι → ordinal) :
(ordinal.type r).bsup (ordinal.bfamily_of_family' r f) = (ordinal.type r').bsup (ordinal.bfamily_of_family' r' f)
source
@[simp]
theorem ordinal.bsup_eq_sup {ι : Type u_1} (f : ι → ordinal) :
(ordinal.type well_ordering_rel).bsup (ordinal.bfamily_of_family f) = ordinal.sup f
source
theorem ordinal.bsup_le_iff {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {a : ordinal} :
o.bsup f ≤ a ↔ ∀ (i : ordinal) (h : i < o), f i h ≤ a
source
theorem ordinal.bsup_le {o : ordinal} {f : Π (b : ordinal), b < o → ordinal} {a : ordinal} :
(∀ (i : ordinal) (h : i < o), f i h ≤ a) → o.bsup f ≤ a
source
theorem ordinal.le_bsup {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) (i : ordinal) (h : i < o) :
f i h ≤ o.bsup f
source
theorem ordinal.lt_bsup {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) {a : ordinal} :
a < o.bsup f ↔ ∃ (i : ordinal) (hi : i < o), a < f i hi
source
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))
source
theorem ordinal.lt_bsup_of_ne_bsup {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} :
(∀ (i : ordinal) (h : i < o), f i h ≠ o.bsup f) ↔ ∀ (i : ordinal) (h : i < o), f i h < o.bsup f
source
theorem ordinal.bsup_not_succ_of_ne_bsup {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} (hf : ∀ {i : ordinal} (h : i < o), f i h ≠ o.bsup f) (a : ordinal) :
a < o.bsup f → a.succ < o.bsup f
source
@[simp]
theorem ordinal.bsup_eq_zero_iff {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} :
o.bsup f = 0 ↔ ∀ (i : ordinal) (hi : i < o), f i hi = 0
source
theorem ordinal.lt_bsup_of_limit {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 : ∀ (a : ordinal), a < o → a.succ < o) (i : ordinal) (h : i < o) :
f i h < o.bsup f
source
theorem ordinal.bsup_zero {o : ordinal} (ho : o = 0) (f : Π (a : ordinal), a < o → ordinal) :
o.bsup f = 0
source
theorem ordinal.bsup_const {o : ordinal} (ho : o ≠ 0) (a : ordinal) :
o.bsup (λ (_x : ordinal) (_x : _x < o), a) = a
source
theorem ordinal.bsup_le_of_brange_subset {o : ordinal} {o' : ordinal} {f : Π (a : ordinal), a < o → ordinal} {g : Π (a : ordinal), a < o' → ordinal} (h : o.brange f ⊆ o'.brange g) :
o.bsup f ≤ o'.bsup g
source
theorem ordinal.bsup_eq_of_brange_eq {o : ordinal} {o' : ordinal} {f : Π (a : ordinal), a < o → ordinal} {g : Π (a : ordinal), a < o' → ordinal} (h : o.brange f = o'.brange g) :
o.bsup f = o'.bsup g
source
noncomputable def ordinal.lsub {ι : Type u_1} (f : ι → ordinal) :
ordinal

The least strict upper bound of a family of ordinals.

Equations
source
@[simp]
theorem ordinal.sup_eq_lsub {ι : Type u_1} (f : ι → ordinal) :
ordinal.sup (ordinal.succ ∘ f) = ordinal.lsub f
source
theorem ordinal.lsub_le_iff {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
ordinal.lsub f ≤ a ↔ ∀ (i : ι), f i < a
source
theorem ordinal.lsub_le {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
(∀ (i : ι), f i < a) → ordinal.lsub f ≤ a
source
theorem ordinal.lt_lsub {ι : Type u_1} (f : ι → ordinal) (i : ι) :
f i < ordinal.lsub f
source
theorem ordinal.lt_lsub_iff {ι : Type u_1} {f : ι → ordinal} {a : ordinal} :
a < ordinal.lsub f ↔ ∃ (i : ι), a ≤ f i
source
theorem ordinal.sup_le_lsub {ι : Type u_1} (f : ι → ordinal) :
ordinal.sup f ≤ ordinal.lsub f
source
theorem ordinal.lsub_le_sup_succ {ι : Type u_1} (f : ι → ordinal) :
ordinal.lsub f ≤ (ordinal.sup f).succ
source
theorem ordinal.sup_eq_lsub_or_sup_succ_eq_lsub {ι : Type u_1} (f : ι → ordinal) :
ordinal.sup f = ordinal.lsub f ∨ (ordinal.sup f).succ = ordinal.lsub f
source
theorem ordinal.sup_succ_le_lsub {ι : Type u_1} (f : ι → ordinal) :
(ordinal.sup f).succ ≤ ordinal.lsub f ↔ ∃ (i : ι), f i = ordinal.sup f
source
theorem ordinal.sup_succ_eq_lsub {ι : Type u_1} (f : ι → ordinal) :
(ordinal.sup f).succ = ordinal.lsub f ↔ ∃ (i : ι), f i = ordinal.sup f
source
theorem ordinal.sup_eq_lsub_iff_succ {ι : Type u_1} (f : ι → ordinal) :
ordinal.sup f = ordinal.lsub f ↔ ∀ (a : ordinal), a < ordinal.lsub f → a.succ < ordinal.lsub f
source
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
source
theorem ordinal.lsub_empty {ι : Type u_1} [h : is_empty ι] (f : ι → ordinal) :
ordinal.lsub f = 0
source
theorem ordinal.lsub_pos {ι : Type u_1} [h : nonempty ι] (f : ι → ordinal) :
0 < ordinal.lsub f
source
@[simp]
theorem ordinal.lsub_eq_zero_iff {ι : Type u_1} {f : ι → ordinal} :
ordinal.lsub f = 0 ↔ is_empty ι
source
theorem ordinal.lsub_const {ι : Type u_1} [hι : nonempty ι] (o : ordinal) :
ordinal.lsub (λ (_x : ι), o) = o + 1
source
theorem ordinal.lsub_le_of_range_subset {ι : Type u} {ι' : Type v} {f : ι → ordinal} {g : ι' → ordinal} (h : set.range f ⊆ set.range g) :
ordinal.lsub f ≤ ordinal.lsub g
source
theorem ordinal.lsub_eq_of_range_eq {ι : Type u} {ι' : Type v} {f : ι → ordinal} {g : ι' → ordinal} (h : set.range f = set.range g) :
ordinal.lsub f = ordinal.lsub g
source
theorem ordinal.lsub_not_mem_range {ι : Type u_1} (f : ι → ordinal) :
ordinal.lsub f ∉ set.range f
source
theorem ordinal.nonempty_compl_range {ι : Type u} (f : ι → ordinal) :
(set.range f)ᶜ.nonempty
source
@[simp]
theorem ordinal.lsub_typein (o : ordinal) :
ordinal.lsub (ordinal.typein has_lt.lt) = o
source
theorem ordinal.sup_typein_limit {o : ordinal} (ho : ∀ (a : ordinal), a < o → a.succ < o) :
ordinal.sup (ordinal.typein has_lt.lt) = o
source
@[simp]
theorem ordinal.sup_typein_succ {o : ordinal} :
ordinal.sup (ordinal.typein has_lt.lt) = o
source
noncomputable def ordinal.blsub (o : ordinal) (f : Π (a : ordinal), a < o → ordinal) :
ordinal

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
source
@[simp]
theorem ordinal.bsup_eq_blsub (o : ordinal) (f : Π (a : ordinal), a < o → ordinal) :
o.bsup (λ (a : ordinal) (ha : a < o), (f a ha).succ) = o.blsub f
source
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 < o → ordinal) :
ordinal.lsub (ordinal.family_of_bfamily' r ho f) = o.blsub f
source
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 < o → ordinal) :
ordinal.lsub (ordinal.family_of_bfamily' r ho f) = ordinal.lsub (ordinal.family_of_bfamily' r' ho' f)
source
@[simp]
theorem ordinal.lsub_eq_blsub {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
ordinal.lsub (o.family_of_bfamily f) = o.blsub f
source
@[simp]
theorem ordinal.blsub_eq_lsub' {ι : Type u_1} (r : ι → ι → Prop) [is_well_order ι r] (f : ι → ordinal) :
(ordinal.type r).blsub (ordinal.bfamily_of_family' r f) = ordinal.lsub f
source
theorem ordinal.blsub_eq_blsub {ι : Type u} (r r' : ι → ι → Prop) [is_well_order ι r] [is_well_order ι r'] (f : ι → ordinal) :
(ordinal.type r).blsub (ordinal.bfamily_of_family' r f) = (ordinal.type r').blsub (ordinal.bfamily_of_family' r' f)
source
@[simp]
theorem ordinal.blsub_eq_lsub {ι : Type u_1} (f : ι → ordinal) :
(ordinal.type well_ordering_rel).blsub (ordinal.bfamily_of_family f) = ordinal.lsub f
source
theorem ordinal.blsub_le_iff {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {a : ordinal} :
o.blsub f ≤ a ↔ ∀ (i : ordinal) (h : i < o), f i h < a
source
theorem ordinal.blsub_le {o : ordinal} {f : Π (b : ordinal), b < o → ordinal} {a : ordinal} :
(∀ (i : ordinal) (h : i < o), f i h < a) → o.blsub f ≤ a
source
theorem ordinal.lt_blsub {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) (i : ordinal) (h : i < o) :
f i h < o.blsub f
source
theorem ordinal.lt_blsub_iff {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {a : ordinal} :
a < o.blsub f ↔ ∃ (i : ordinal) (hi : i < o), a ≤ f i hi
source
theorem ordinal.bsup_le_blsub {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
o.bsup f ≤ o.blsub f
source
theorem ordinal.blsub_le_bsup_succ {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
o.blsub f ≤ (o.bsup f).succ
source
theorem ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
o.bsup f = o.blsub f ∨ (o.bsup f).succ = o.blsub f
source
theorem ordinal.bsup_succ_le_blsub {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
(o.bsup f).succ ≤ o.blsub f ↔ ∃ (i : ordinal) (hi : i < o), f i hi = o.bsup f
source
theorem ordinal.bsup_succ_eq_blsub {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
(o.bsup f).succ = o.blsub f ↔ ∃ (i : ordinal) (hi : i < o), f i hi = o.bsup f
source
theorem ordinal.bsup_eq_blsub_iff_succ {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
o.bsup f = o.blsub f ↔ ∀ (a : ordinal), a < o.blsub f → a.succ < o.blsub f
source
theorem ordinal.bsup_eq_blsub_iff_lt_bsup {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
o.bsup f = o.blsub f ↔ ∀ (i : ordinal) (hi : i < o), f i hi < o.bsup f
source
theorem ordinal.bsup_eq_blsub_of_lt_succ_limit {o : ordinal} (ho : o.is_limit) {f : Π (a : ordinal), a < o → ordinal} (hf : ∀ (a : ordinal) (ha : a < o), f a ha < f a.succ _) :
o.bsup f = o.blsub f
source
@[simp]
theorem ordinal.blsub_eq_zero_iff {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} :
o.blsub f = 0 ↔ o = 0
source
theorem ordinal.blsub_zero {o : ordinal} (ho : o = 0) (f : Π (a : ordinal), a < o → ordinal) :
o.blsub f = 0
source
theorem ordinal.blsub_pos {o : ordinal} (ho : 0 < o) (f : Π (a : ordinal), a < o → ordinal) :
0 < o.blsub f
source
theorem ordinal.blsub_type {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (f : Π (a : ordinal), a < ordinal.type r → ordinal) :
(ordinal.type r).blsub f = ordinal.lsub (λ (a : α), f (ordinal.typein r a) _)
source
theorem ordinal.blsub_const {o : ordinal} (ho : o ≠ 0) (a : ordinal) :
o.blsub (λ (_x : ordinal) (_x : _x < o), a) = a + 1
source
@[simp]
theorem ordinal.blsub_id (o : ordinal) :
o.blsub (λ (x : ordinal) (_x : x < o), x) = o
source
theorem ordinal.bsup_id_limit {o : ordinal} :
(∀ (a : ordinal), a < o → a.succ < o) → o.bsup (λ (x : ordinal) (_x : x < o), x) = o
source
@[simp]
theorem ordinal.bsup_id_succ (o : ordinal) :
o.succ.bsup (λ (x : ordinal) (_x : x < o.succ), x) = o
source
theorem ordinal.blsub_le_of_brange_subset {o : ordinal} {o' : ordinal} {f : Π (a : ordinal), a < o → ordinal} {g : Π (a : ordinal), a < o' → ordinal} (h : o.brange f ⊆ o'.brange g) :
o.blsub f ≤ o'.blsub g
source
theorem ordinal.blsub_eq_of_brange_eq {o : ordinal} {o' : ordinal} {f : Π (a : ordinal), a < o → ordinal} {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
source
theorem ordinal.bsup_comp {o o' : ordinal} {f : Π (a : ordinal), a < o → ordinal} (hf : ∀ {i j : ordinal} (hi : i < o) (hj : j < o), i ≤ j → f 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
source
theorem ordinal.blsub_comp {o o' : ordinal} {f : Π (a : ordinal), a < o → ordinal} (hf : ∀ {i j : ordinal} (hi : i < o) (hj : j < o), i ≤ j → f 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
source
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
source
theorem ordinal.is_normal.blsub_eq {f : ordinal → ordinal} (H : ordinal.is_normal f) {o : ordinal} (h : o.is_limit) :
o.blsub (λ (x : ordinal) (_x : x < o), f x) = f o
source
theorem ordinal.is_normal_iff_lt_succ_and_bsup_eq {f : ordinal → ordinal} :
ordinal.is_normal f ↔ (∀ (a : ordinal), f a < f a.succ) ∧ ∀ (o : ordinal), o.is_limit → o.bsup (λ (x : ordinal) (_x : x < o), f x) = f o
source
theorem ordinal.is_normal_iff_lt_succ_and_blsub_eq {f : ordinal → ordinal} :
ordinal.is_normal f ↔ (∀ (a : ordinal), f a < f a.succ) ∧ ∀ (o : ordinal), o.is_limit → o.blsub (λ (x : ordinal) (_x : x < o), f x) = f o
source
theorem ordinal.is_normal.eq_iff_zero_and_succ {f : ordinal → ordinal} (hf : ordinal.is_normal f) {g : ordinal → ordinal} (hg : ordinal.is_normal g) :
f = g ↔ f 0 = g 0 ∧ ∀ (a : ordinal), f a = g a → f a.succ = g a.succ

Minimum excluded ordinals #

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

The minimum excluded ordinal in a family of ordinals.

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

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
source
theorem ordinal.bmex_not_mem_brange {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
o.bmex f ∉ o.brange f
source
theorem ordinal.ne_bmex {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) {i : ordinal} (hi : i < o) :
f i hi ≠ o.bmex f
source
theorem ordinal.bmex_le_of_ne {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {a : ordinal} (ha : ∀ (i : ordinal) (hi : i < o), f i hi ≠ a) :
o.bmex f ≤ a
source
theorem ordinal.exists_of_lt_bmex {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {a : ordinal} (ha : a < o.bmex f) :
∃ (i : ordinal) (hi : i < o), f i hi = a
source
theorem ordinal.bmex_le_blsub {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
o.bmex f ≤ o.blsub f
source
theorem ordinal.bmex_monotone {o o' : ordinal} {f : Π (a : ordinal), a < o → ordinal} {g : Π (a : ordinal), a < o' → ordinal} (h : o.brange f ⊆ o'.brange g) :
o.bmex f ≤ o'.bmex g
source
theorem ordinal.bmex_lt_ord_succ_card {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
o.bmex f < o.card.succ.ord

Results about injectivity and surjectivity #

source
theorem not_surjective_of_ordinal {α : Type u} (f : α → ordinal) :
¬function.surjective f
source
theorem not_injective_of_ordinal {α : Type u} (f : ordinal → α) :
¬function.injective f
source
theorem not_surjective_of_ordinal_of_small {α : Type v} [small α] (f : α → ordinal) :
¬function.surjective f
source
theorem not_injective_of_ordinal_of_small {α : Type v} [small α] (f : ordinal → α) :
¬function.injective f
source
theorem not_small_ordinal  :
¬small 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 #

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

Enumerator function for an unbounded set of ordinals.

Equations
source
theorem ordinal.enum_ord_def' {S : set ordinal} (o : ordinal) :
ordinal.enum_ord S o = 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.

source
theorem ordinal.enum_ord_def'_nonempty {S : set ordinal} (hS : set.unbounded has_lt.lt S) (a : ordinal) :
(S ∩ set.Ici a).nonempty

The set in enum_ord_def' is nonempty.

source
theorem ordinal.enum_ord_mem {S : set ordinal} (hS : set.unbounded has_lt.lt S) (o : ordinal) :
ordinal.enum_ord S o ∈ S
source
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
source
theorem ordinal.enum_ord_strict_mono {S : set ordinal} (hS : set.unbounded has_lt.lt S) :
strict_mono (ordinal.enum_ord S)
source
theorem ordinal.enum_ord_def {S : set ordinal} (o : ordinal) :
ordinal.enum_ord S o = Inf (S ∩ {b : ordinal | ∀ (c : ordinal), c < o → ordinal.enum_ord S c < b})

A more workable definition for enum_ord.

source
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 < o → ordinal.enum_ord S c < x}.nonempty

The set in enum_ord_def is nonempty.

source
@[simp]
theorem ordinal.enum_ord_range {f : ordinal → ordinal} (hf : strict_mono f) :
ordinal.enum_ord (set.range f) = f
source
@[simp]
theorem ordinal.enum_ord_univ  :
ordinal.enum_ord set.univ = id
source
@[simp]
theorem ordinal.enum_ord_zero {S : set ordinal} :
ordinal.enum_ord S 0 = Inf S
source
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) :
ordinal.enum_ord S b.succ ≤ a
source
theorem ordinal.enum_ord_le_of_subset {S T : set ordinal} (hS : set.unbounded has_lt.lt S) (hST : S ⊆ T) (a : ordinal) :
ordinal.enum_ord T a ≤ ordinal.enum_ord S a
source
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
source
noncomputable def ordinal.enum_ord_order_iso {S : set ordinal} (hS : set.unbounded has_lt.lt S) :
ordinal ≃o ↥S

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

Equations
source
theorem ordinal.range_enum_ord {S : set ordinal} (hS : set.unbounded has_lt.lt S) :
set.range (ordinal.enum_ord S) = S
source
theorem ordinal.eq_enum_ord {S : set ordinal} (f : ordinal → ordinal) (hS : set.unbounded has_lt.lt S) :
strict_mono f ∧ set.range f = S ↔ f = ordinal.enum_ord S

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

Ordinal exponential #

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

The ordinal exponential, defined by transfinite recursion.

Equations
source
@[protected, instance]
noncomputable def ordinal.has_pow  :
has_pow ordinal ordinal
Equations
source
theorem ordinal.zero_opow' (a : ordinal) :
0 ^ a = 1 - a
source
@[simp]
theorem ordinal.zero_opow {a : ordinal} (a0 : a ≠ 0) :
0 ^ a = 0
source
@[simp]
theorem ordinal.opow_zero (a : ordinal) :
a ^ 0 = 1
source
@[simp]
theorem ordinal.opow_succ (a b : ordinal) :
a ^ b.succ = (a ^ b) * a
source
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)
source
theorem ordinal.opow_le_of_limit {a b c : ordinal} (a0 : a ≠ 0) (h : b.is_limit) :
a ^ b ≤ c ↔ ∀ (b' : ordinal), b' < b → a ^ b' ≤ c
source
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'
source
@[simp]
theorem ordinal.opow_one (a : ordinal) :
a ^ 1 = a
source
@[simp]
theorem ordinal.one_opow (a : ordinal) :
1 ^ a = 1
source
theorem ordinal.opow_pos {a : ordinal} (b : ordinal) (a0 : 0 < a) :
0 < a ^ b
source
theorem ordinal.opow_ne_zero {a : ordinal} (b : ordinal) (a0 : a ≠ 0) :
a ^ b ≠ 0
source
theorem ordinal.opow_is_normal {a : ordinal} (h : 1 < a) :
ordinal.is_normal (λ (_y : ordinal), a ^ _y)
source
theorem ordinal.opow_lt_opow_iff_right {a b c : ordinal} (a1 : 1 < a) :
a ^ b < a ^ c ↔ b < c
source
theorem ordinal.opow_le_opow_iff_right {a b c : ordinal} (a1 : 1 < a) :
a ^ b ≤ a ^ c ↔ b ≤ c
source
theorem ordinal.opow_right_inj {a b c : ordinal} (a1 : 1 < a) :
a ^ b = a ^ c ↔ b = c
source
theorem ordinal.opow_is_limit {a b : ordinal} (a1 : 1 < a) :
b.is_limit → (a ^ b).is_limit
source
theorem ordinal.opow_is_limit_left {a b : ordinal} (l : a.is_limit) (hb : b ≠ 0) :
(a ^ b).is_limit
source
theorem ordinal.opow_le_opow_right {a b c : ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) :
a ^ b ≤ a ^ c
source
theorem ordinal.opow_le_opow_left {a b : ordinal} (c : ordinal) (ab : a ≤ b) :
a ^ c ≤ b ^ c
source
theorem ordinal.left_le_opow (a : ordinal) {b : ordinal} (b1 : 0 < b) :
a ≤ a ^ b
source
theorem ordinal.right_le_opow {a : ordinal} (b : ordinal) (a1 : 1 < a) :
b ≤ a ^ b
source
theorem ordinal.opow_lt_opow_left_of_succ {a b c : ordinal} (ab : a < b) :
a ^ c.succ < b ^ c.succ
source
theorem ordinal.opow_add (a b c : ordinal) :
a ^ (b + c) = (a ^ b) * a ^ c
source
theorem ordinal.opow_one_add (a b : ordinal) :
a ^ (1 + b) = a * a ^ b
source
theorem ordinal.opow_dvd_opow (a : ordinal) {b c : ordinal} (h : b ≤ c) :
a ^ b ∣ a ^ c
source
theorem ordinal.opow_dvd_opow_iff {a b c : ordinal} (a1 : 1 < a) :
a ^ b ∣ a ^ c ↔ b ≤ c
source
theorem ordinal.opow_mul (a b c : ordinal) :
a ^ b * c = (a ^ b) ^ c

Ordinal logarithm #

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

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

Equations
source
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.

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

The Cantor normal form #

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

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

Equations
source
@[simp]
theorem ordinal.CNF_rec_zero {b : ordinal} (b0 : b ≠ 0) {C : ordinal → Sort u_2} {H0 : C 0} {H : Π (o : ordinal), o ≠ 0 → C (o % b ^ b.log o) → C o} :
ordinal.CNF_rec b0 H0 H 0 = H0
source
@[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 → 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))
source
noncomputable def ordinal.CNF (b o : ordinal) :
list (ordinal × ordinal)

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

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

Equations
source
@[simp]
theorem ordinal.zero_CNF (o : ordinal) :
0.CNF o = list.nil
source
@[simp]
theorem ordinal.CNF_zero (b : ordinal) :
b.CNF 0 = list.nil
source
theorem ordinal.CNF_ne_zero {b o : ordinal} (b0 : b ≠ 0) (o0 : o ≠ 0) :
b.CNF o = (b.log o, o / b ^ b.log o) :: b.CNF (o % b ^ b.log o)
source
@[simp]
theorem ordinal.one_CNF {o : ordinal} (o0 : o ≠ 0) :
1.CNF o = [(0, o)]
source
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 (b.CNF o) = o
source
theorem ordinal.CNF_pairwise (b o : ordinal) :
list.pairwise (λ (p q : ordinal × ordinal), q.fst < p.fst) (b.CNF o)
source
theorem ordinal.CNF_fst_le_log {b o : ordinal} {p : ordinal × ordinal} :
p ∈ b.CNF o → p.fst ≤ b.log o
source
theorem ordinal.CNF_fst_le {b o : ordinal} {p : ordinal × ordinal} (hp : p ∈ b.CNF o) :
p.fst ≤ o
source
theorem ordinal.CNF_snd_lt {b o : ordinal} (b1 : 1 < b) {p : ordinal × ordinal} (hp : p ∈ b.CNF o) :
p.snd < b
source
theorem ordinal.CNF_lt_snd {b o : ordinal} (b1 : 1 < b) {p : ordinal × ordinal} (hp : p ∈ b.CNF o) :
0 < p.snd
source
theorem ordinal.CNF_sorted (b o : ordinal) :
list.sorted gt (list.map prod.fst (b.CNF o))

Casting naturals into ordinals, compatibility with operations #

source
@[simp]
theorem ordinal.nat_cast_mul {m n : ℕ} :
↑m * n = (↑m) * ↑n
source
@[simp]
theorem ordinal.nat_cast_opow {m n : ℕ} :
↑(m ^ n) = ↑m ^ ↑n
source
@[simp]
theorem ordinal.nat_cast_le {m n : ℕ} :
↑m ≤ ↑n ↔ m ≤ n
source
@[simp]
theorem ordinal.nat_cast_lt {m n : ℕ} :
↑m < ↑n ↔ m < n
source
@[simp]
theorem ordinal.nat_cast_inj {m n : ℕ} :
↑m = ↑n ↔ m = n
source
@[simp]
theorem ordinal.nat_cast_eq_zero {n : ℕ} :
↑n = 0 ↔ n = 0
source
theorem ordinal.nat_cast_ne_zero {n : ℕ} :
↑n ≠ 0 ↔ n ≠ 0
source
@[simp]
theorem ordinal.nat_cast_pos {n : ℕ} :
0 < ↑n ↔ 0 < n
source
@[simp]
theorem ordinal.nat_cast_sub {m n : ℕ} :
↑(m - n) = ↑m - ↑n
source
@[simp]
theorem ordinal.nat_cast_div {m n : ℕ} :
↑(m / n) = ↑m / ↑n
source
@[simp]
theorem ordinal.nat_cast_mod {m n : ℕ} :
↑(m % n) = ↑m % ↑n
source
@[simp]
theorem ordinal.nat_le_card {o : ordinal} {n : ℕ} :
↑n ≤ o.card ↔ ↑n ≤ o
source
@[simp]
theorem ordinal.nat_lt_card {o : ordinal} {n : ℕ} :
↑n < o.card ↔ ↑n < o
source
@[simp]
theorem ordinal.card_lt_nat {o : ordinal} {n : ℕ} :
o.card < ↑n ↔ o < ↑n
source
@[simp]
theorem ordinal.card_le_nat {o : ordinal} {n : ℕ} :
o.card ≤ ↑n ↔ o ≤ ↑n
source
@[simp]
theorem ordinal.card_eq_nat {o : ordinal} {n : ℕ} :
o.card = ↑n ↔ o = ↑n
source
@[simp]
theorem ordinal.type_fin (n : ℕ) :
ordinal.type has_lt.lt = ↑n
source
@[simp]
theorem ordinal.lift_nat_cast (n : ℕ) :
↑n.lift = ↑n
source
theorem ordinal.lift_type_fin (n : ℕ) :
(ordinal.type has_lt.lt).lift = ↑n
source
theorem ordinal.type_fintype {α : Type u_1} (r : α → α → Prop) [is_well_order α r] [fintype α] :
ordinal.type r = ↑(fintype.card α)

Properties of omega #

source
@[simp]
theorem cardinal.ord_omega  :
ω.ord = ω
source
@[simp]
theorem cardinal.add_one_of_omega_le {c : cardinal} (h : ω ≤ c) :
c + 1 = c
source
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'
source
theorem ordinal.lt_omega {o : ordinal} :
o < ω ↔ ∃ (n : ℕ), o = ↑n
source
theorem ordinal.nat_lt_omega (n : ℕ) :
↑n < ω
source
theorem ordinal.omega_pos  :
0 < ω
source
theorem ordinal.omega_ne_zero  :
ω ≠ 0
source
theorem ordinal.one_lt_omega  :
1 < ω
source
theorem ordinal.omega_is_limit  :
ω.is_limit
source
theorem ordinal.omega_le {o : ordinal} :
ω ≤ o ↔ ∀ (n : ℕ), ↑n ≤ o
source
@[simp]
theorem ordinal.sup_nat_cast  :
ordinal.sup nat.cast = ω
source
theorem ordinal.nat_lt_limit {o : ordinal} (h : o.is_limit) (n : ℕ) :
↑n < o
source
theorem ordinal.omega_le_of_is_limit {o : ordinal} (h : o.is_limit) :
ω ≤ o
source
theorem ordinal.is_limit_iff_omega_dvd {a : ordinal} :
a.is_limit ↔ a ≠ 0 ∧ ω ∣ a
source
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
source
theorem ordinal.add_mul_succ {a b : ordinal} (c : ordinal) (ba : b + a = a) :
(a + b) * c.succ = a * c.succ + b
source
theorem ordinal.add_mul_limit {a b c : ordinal} (ba : b + a = a) (l : c.is_limit) :
(a + b) * c = a * c
source
theorem ordinal.add_le_of_forall_add_lt {a b c : ordinal} (hb : 0 < b) (h : ∀ (d : ordinal), d < b → a + d < c) :
a + b ≤ c
source
theorem ordinal.is_normal.apply_omega {f : ordinal → ordinal} (hf : ordinal.is_normal f) :
ordinal.sup (f ∘ nat.cast) = f ω
source
@[simp]
theorem ordinal.sup_add_nat (o : ordinal) :
ordinal.sup (λ (n : ℕ), o + ↑n) = o + ω
source
@[simp]
theorem ordinal.sup_mul_nat (o : ordinal) :
ordinal.sup (λ (n : ℕ), o * ↑n) = o * ω
source
theorem ordinal.sup_opow_nat {o : ordinal} (ho : 0 < o) :
ordinal.sup (λ (n : ℕ), o ^ ↑n) = o ^ ω

Fixed points of normal functions #

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

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

Equations
source
theorem ordinal.nfp_le_iff {f : ordinal → ordinal} {a b : ordinal} :
ordinal.nfp f a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
source
theorem ordinal.nfp_le {f : ordinal → ordinal} {a b : ordinal} :
(∀ (n : ℕ), f^[n] a ≤ b) → ordinal.nfp f a ≤ b
source
theorem ordinal.iterate_le_nfp (f : ordinal → ordinal) (a : ordinal) (n : ℕ) :
f^[n] a ≤ ordinal.nfp f a
source
theorem ordinal.le_nfp_self (f : ordinal → ordinal) (a : ordinal) :
a ≤ ordinal.nfp f a
source
theorem ordinal.lt_nfp {f : ordinal → ordinal} {a b : ordinal} :
a < ordinal.nfp f b ↔ ∃ (n : ℕ), a < f^[n] b
source
@[protected]
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
source
@[protected]
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
source
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
source
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
source
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
source
theorem ordinal.nfp_eq_self {f : ordinal → ordinal} {a : ordinal} (h : f a = a) :
ordinal.nfp f a = a
source
@[protected]
theorem ordinal.monotone.nfp {f : ordinal → ordinal} (hf : monotone f) :
monotone (ordinal.nfp f)
source
theorem ordinal.is_normal.nfp_unbounded {f : ordinal → ordinal} (H : ordinal.is_normal f) :
set.unbounded has_lt.lt (function.fixed_points f)

Fixed point lemma for normal functions: the fixed points of a normal function are unbounded.

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

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

Equations
source
@[simp]
theorem ordinal.deriv_zero (f : ordinal → ordinal) :
ordinal.deriv f 0 = ordinal.nfp f 0
source
@[simp]
theorem ordinal.deriv_succ (f : ordinal → ordinal) (o : ordinal) :
ordinal.deriv f o.succ = ordinal.nfp f (ordinal.deriv f o).succ
source
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)
source
theorem ordinal.deriv_is_normal (f : ordinal → ordinal) :
ordinal.is_normal (ordinal.deriv f)
source
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
source
theorem ordinal.is_normal.le_iff_deriv {f : ordinal → ordinal} (H : ordinal.is_normal f) {a : ordinal} :
f a ≤ a ↔ ∃ (o : ordinal), ordinal.deriv f o = a
source
theorem ordinal.is_normal.apply_eq_self_iff_deriv {f : ordinal → ordinal} (H : ordinal.is_normal f) {a : ordinal} :
f a = a ↔ ∃ (o : ordinal), ordinal.deriv f o = a
source
theorem ordinal.deriv_eq_enum_fp {f : ordinal → ordinal} (H : ordinal.is_normal f) :
ordinal.deriv f = ordinal.enum_ord (function.fixed_points f)

deriv f is the fixed point enumerator of f.

source
theorem ordinal.deriv_eq_id_of_nfp_eq_id {f : ordinal → ordinal} (h : ordinal.nfp f = id) :
ordinal.deriv f = id

Fixed points of addition #

source
@[simp]
theorem ordinal.nfp_add_zero (a : ordinal) :
ordinal.nfp (has_add.add a) 0 = a * ω
source
theorem ordinal.nfp_add_eq_mul_omega {a b : ordinal} (hba : b ≤ a * ω) :
ordinal.nfp (has_add.add a) b = a * ω
source
theorem ordinal.add_eq_right_iff_mul_omega_le {a b : ordinal} :
a + b = b ↔ a * ω ≤ b
source
theorem ordinal.add_le_right_iff_mul_omega_le {a b : ordinal} :
a + b ≤ b ↔ a * ω ≤ b
source
theorem ordinal.deriv_add_eq_mul_omega_add (a b : ordinal) :
ordinal.deriv (has_add.add a) b = a * ω + b

Fixed points of multiplication #

source
@[simp]
theorem ordinal.nfp_mul_one {a : ordinal} (ha : 0 < a) :
ordinal.nfp (has_mul.mul a) 1 = a ^ ω
source
@[simp]
theorem ordinal.nfp_mul_zero (a : ordinal) :
ordinal.nfp (has_mul.mul a) 0 = 0
source
@[simp]
theorem ordinal.nfp_zero_mul  :
ordinal.nfp (has_mul.mul 0) = id
source
@[simp]
theorem ordinal.deriv_mul_zero  :
ordinal.deriv (has_mul.mul 0) = id
source
theorem ordinal.nfp_mul_eq_opow_omega {a b : ordinal} (hb : 0 < b) (hba : b ≤ a ^ ω) :
ordinal.nfp (has_mul.mul a) b = a ^ ω
source
theorem ordinal.eq_zero_or_opow_omega_le_of_mul_eq_right {a b : ordinal} (hab : a * b = b) :
b = 0 ∨ a ^ ω ≤ b
source
theorem ordinal.mul_eq_right_iff_opow_omega_dvd {a b : ordinal} :
a * b = b ↔ a ^ ω ∣ b
source
theorem ordinal.mul_le_right_iff_opow_omega_dvd {a b : ordinal} (ha : 0 < a) :
a * b ≤ b ↔ a ^ ω ∣ b
source
theorem ordinal.nfp_mul_opow_omega_add {a c : ordinal} (b : ordinal) (ha : 0 < a) (hc : 0 < c) (hca : c ≤ a ^ ω) :
ordinal.nfp (has_mul.mul a) ((a ^ ω) * b + c) = (a ^ ω) * b.succ
source
theorem ordinal.deriv_mul_eq_opow_omega_mul {a : ordinal} (ha : 0 < a) (b : ordinal) :
ordinal.deriv (has_mul.mul a) b = (a ^ ω) * b