mathlib3 documentation

set_theory.ordinal.arithmetic

Ordinal arithmetic #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
order.succ o = o + 1 is the successor of o.
pred o if the predecessor of o. If o is not a successor, we set pred o = o.

We discuss the properties of casts of natural numbers of and of ω with respect to these operations.

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

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

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

Further properties of addition on ordinals #

@[simp]

theorem ordinal.lift_add (a b : ordinal) :

(a + b).lift = a.lift + b.lift

@[simp]

theorem ordinal.lift_succ (a : ordinal) :

(order.succ a).lift = order.succ a.lift

@[protected, instance]

def ordinal.add_contravariant_class_le :

contravariant_class ordinal ordinal has_add.add has_le.le

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

a + b = a + c ↔ b = c

@[protected, instance]

def ordinal.add_covariant_class_lt :

covariant_class ordinal ordinal has_add.add has_lt.lt

@[protected, instance]

def ordinal.add_contravariant_class_lt :

contravariant_class ordinal ordinal has_add.add has_lt.lt

@[protected, instance]

def ordinal.add_swap_contravariant_class_lt :

contravariant_class ordinal ordinal (function.swap has_add.add) has_lt.lt

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

theorem ordinal.add_eq_zero_iff {a b : ordinal} :

a + b = 0 ↔ a = 0 ∧ b = 0

theorem ordinal.left_eq_zero_of_add_eq_zero {a b : ordinal} (h : a + b = 0) :

a = 0

theorem ordinal.right_eq_zero_of_add_eq_zero {a b : ordinal} (h : a + b = 0) :

b = 0

The predecessor of an ordinal #

noncomputable def ordinal.pred (o : ordinal) :

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

Equations

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

@[simp]

theorem ordinal.pred_succ (o : ordinal) :

(order.succ o).pred = o

theorem ordinal.pred_le_self (o : ordinal) :

theorem ordinal.pred_eq_iff_not_succ {o : ordinal} :

o.pred = o ↔ ¬∃ (a : ordinal), o = order.succ a

theorem ordinal.pred_eq_iff_not_succ' {o : ordinal} :

o.pred = o ↔ ∀ (a : ordinal), o ≠ order.succ a

theorem ordinal.pred_lt_iff_is_succ {o : ordinal} :

o.pred < o ↔ ∃ (a : ordinal), o = order.succ a

@[simp]

theorem ordinal.pred_zero :

0.pred = 0

theorem ordinal.succ_pred_iff_is_succ {o : ordinal} :

order.succ o.pred = o ↔ ∃ (a : ordinal), o = order.succ a

theorem ordinal.succ_lt_of_not_succ {o b : ordinal} (h : ¬∃ (a : ordinal), o = order.succ a) :

order.succ b < o ↔ b < o

theorem ordinal.lt_pred {a b : ordinal} :

a < b.pred ↔ order.succ a < b

theorem ordinal.pred_le {a b : ordinal} :

a.pred ≤ b ↔ a ≤ order.succ b

@[simp]

theorem ordinal.lift_is_succ {o : ordinal} :

(∃ (a : ordinal), o.lift = order.succ a) ↔ ∃ (a : ordinal), o = order.succ a

@[simp]

theorem ordinal.lift_pred (o : ordinal) :

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 → order.succ a < o)

theorem ordinal.is_limit.succ_lt {o a : ordinal} (h : o.is_limit) :

a < o → order.succ a < o

theorem ordinal.not_zero_is_limit :

theorem ordinal.not_succ_is_limit (o : ordinal) :

¬(order.succ o).is_limit

theorem ordinal.not_succ_of_is_limit {o : ordinal} (h : o.is_limit) :

¬∃ (a : ordinal), o = order.succ a

theorem ordinal.succ_lt_of_is_limit {o a : ordinal} (h : o.is_limit) :

order.succ a < o ↔ a < o

theorem ordinal.le_succ_of_is_limit {o : ordinal} (h : o.is_limit) {a : ordinal} :

o ≤ order.succ a ↔ 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 = order.succ a) ∨ o.is_limit

noncomputable def ordinal.limit_rec_on {C : ordinal → Sort u_2} (o : ordinal) (H₁ : C 0) (H₂ : Π (o : ordinal), C o → C (order.succ o)) (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.lt_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 = order.succ a) (λ (h : ∃ (a : ordinal), o = order.succ a), _.mpr (H₂ o.pred (IH o.pred _))) (λ (h : ¬∃ (a : ordinal), o = order.succ a), 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 (order.succ o)) (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 (order.succ o)) (H₃ : Π (o : ordinal), o.is_limit → (Π (o' : ordinal), o' < o → C o') → C o) :

(order.succ o).limit_rec_on H₁ H₂ H₃ = H₂ o (o.limit_rec_on H₁ H₂ H₃)

@[simp]

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

@[protected, instance]

noncomputable def ordinal.order_top_out_succ (o : ordinal) :

order_top (quotient.out (order.succ o)).α

Equations

o.order_top_out_succ = {top := (λ (f : subrel has_lt.lt {b : ordinal | b < (ordinal.typein.principal_seg has_lt.lt).top} ≃r has_lt.lt), ⇑f) (ordinal.typein.principal_seg has_lt.lt).subrel_iso ⟨o, _⟩, le_top := _}

theorem ordinal.enum_succ_eq_top {o : ordinal} :

ordinal.enum has_lt.lt o _ = ⊤

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 → order.succ a < ordinal.type r) (x : α) :

∃ (y : α), r x y

theorem ordinal.out_no_max_of_succ_lt {o : ordinal} (ho : ∀ (a : ordinal), a < o → order.succ a < o) :

no_max_order (quotient.out o).α

theorem ordinal.bounded_singleton {α : Type u_1} {r : α → α → Prop} [is_well_order α r] (hr : (ordinal.type r).is_limit) (x : α) :

set.bounded r {x}

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

cardinal.mk ↥{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 (order.succ o)) ∧ ∀ (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.strict_mono {f : ordinal → ordinal} (H : ordinal.is_normal f) :

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

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

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

a ≤ f a

theorem ordinal.is_normal.le_set {f : ordinal → ordinal} {o : 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) :

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

theorem ordinal.is_normal.le_set' {α : Type u_1} {f : ordinal → ordinal} {o : ordinal} (H : ordinal.is_normal f) (p : set α) (p0 : p.nonempty) (g : α → ordinal) (b : ordinal) (H₂ : ∀ (o : ordinal), b ≤ o ↔ ∀ (a : α), a ∈ p → g a ≤ o) :

f b ≤ o ↔ ∀ (a : α), a ∈ p → 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 (f ∘ g)

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

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

f a ≤ a ↔ f a = a

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

a + b ≤ c ↔ ∀ (b' : ordinal), b' < 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

theorem ordinal.is_limit.add (a : ordinal) {b : ordinal} :

b.is_limit → (a + b).is_limit

Alias of ordinal.add_is_limit.

Subtraction on ordinals #

theorem ordinal.sub_nonempty {a b : ordinal} :

{o : ordinal | a ≤ b + o}.nonempty

The set in the definition of subtraction is nonempty.

@[protected, instance]

noncomputable def ordinal.has_sub :

has_sub ordinal

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

Equations

ordinal.has_sub = {sub := λ (a b : ordinal), has_Inf.Inf {o : ordinal | a ≤ b + o}}

theorem ordinal.le_add_sub (a b : ordinal) :

a ≤ b + (a - b)

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

a - b ≤ c ↔ a ≤ b + c

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

a < b - c ↔ c + a < b

theorem ordinal.add_sub_cancel (a b : ordinal) :

a + b - a = b

theorem ordinal.sub_eq_of_add_eq {a b c : ordinal} (h : a + b = c) :

c - a = b

theorem ordinal.sub_le_self (a b : ordinal) :

a - b ≤ a

@[protected]

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

b + (a - b) = a

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

c ≤ a - b ↔ b + c ≤ a

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

a - b < c ↔ a < b + c

@[protected, instance]

def ordinal.has_exists_add_of_le :

has_exists_add_of_le ordinal

@[simp]

theorem ordinal.sub_zero (a : ordinal) :

a - 0 = a

@[simp]

theorem ordinal.zero_sub (a : ordinal) :

0 - a = 0

@[simp]

theorem ordinal.sub_self (a : ordinal) :

a - a = 0

@[protected]

theorem ordinal.sub_eq_zero_iff_le {a b : ordinal} :

a - b = 0 ↔ a ≤ b

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

a - b - c = a - (b + c)

@[simp]

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 :

1 + ordinal.omega = ordinal.omega

@[simp]

theorem ordinal.one_add_of_omega_le {o : ordinal} (h : ordinal.omega ≤ 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_prod_lex {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [is_well_order α r] [is_well_order β s] :

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

@[protected, instance]

def ordinal.monoid_with_zero :

monoid_with_zero ordinal

Equations

ordinal.monoid_with_zero = {mul := monoid.mul ordinal.monoid, mul_assoc := _, one := monoid.one ordinal.monoid, one_mul := _, mul_one := _, npow := monoid.npow ordinal.monoid, npow_zero' := _, npow_succ' := _, zero := 0, zero_mul := ordinal.monoid_with_zero._proof_1, mul_zero := ordinal.monoid_with_zero._proof_2}

@[protected, instance]

def ordinal.no_zero_divisors :

no_zero_divisors ordinal

@[simp]

theorem ordinal.lift_mul (a b : ordinal) :

(a * b).lift = a.lift * b.lift

@[simp]

theorem ordinal.card_mul (a b : ordinal) :

(a * b).card = a.card * b.card

@[protected, instance]

def ordinal.left_distrib_class :

left_distrib_class ordinal

Equations

ordinal.left_distrib_class = {left_distrib := ordinal.left_distrib_class._proof_1}

theorem ordinal.mul_succ (a b : ordinal) :

a * order.succ b = a * b + a

@[protected, instance]

def ordinal.mul_covariant_class_le :

covariant_class ordinal ordinal has_mul.mul has_le.le

@[protected, instance]

def ordinal.mul_swap_covariant_class_le :

covariant_class ordinal ordinal (function.swap has_mul.mul) has_le.le

theorem ordinal.le_mul_left (a : ordinal) {b : ordinal} (hb : 0 < b) :

a ≤ a * b

theorem ordinal.le_mul_right (a : ordinal) {b : ordinal} (hb : 0 < b) :

a ≤ b * a

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

a * b ≤ c ↔ ∀ (b' : ordinal), b' < 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

theorem ordinal.smul_eq_mul (n : ℕ) (a : ordinal) :

n • a = a * ↑n

Division on ordinals #

theorem ordinal.div_nonempty {a b : ordinal} (h : b ≠ 0) :

{o : ordinal | a < b * order.succ o}.nonempty

The set in the definition of division is nonempty.

@[protected, instance]

noncomputable def ordinal.has_div :

has_div ordinal

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

Equations

ordinal.has_div = {div := λ (a b : ordinal), dite (b = 0) (λ (h : b = 0), 0) (λ (h : ¬b = 0), has_Inf.Inf {o : ordinal | a < b * order.succ o})}

@[simp]

theorem ordinal.div_zero (a : ordinal) :

a / 0 = 0

theorem ordinal.div_def (a : ordinal) {b : ordinal} (h : b ≠ 0) :

a / b = has_Inf.Inf {o : ordinal | a < b * order.succ o}

theorem ordinal.lt_mul_succ_div (a : ordinal) {b : ordinal} (h : b ≠ 0) :

a < b * order.succ (a / b)

theorem ordinal.lt_mul_div_add (a : ordinal) {b : ordinal} (h : b ≠ 0) :

a < b * (a / b) + b

theorem ordinal.div_le {a b c : ordinal} (b0 : b ≠ 0) :

a / b ≤ c ↔ a < b * order.succ c

theorem ordinal.lt_div {a b c : ordinal} (h : c ≠ 0) :

a < b / c ↔ c * order.succ a ≤ b

theorem ordinal.div_pos {b c : ordinal} (h : c ≠ 0) :

0 < b / c ↔ c ≤ 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.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_dvd.dvd.is_antisymm :

is_antisymm ordinal has_dvd.dvd

@[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

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

theorem ordinal.mod_def (a b : ordinal) :

a % b = a - b * (a / b)

theorem ordinal.mod_le (a b : ordinal) :

a % b ≤ a

@[simp]

theorem ordinal.mod_zero (a : ordinal) :

a % 0 = a

theorem ordinal.mod_eq_of_lt {a b : ordinal} (h : a < b) :

a % b = a

@[simp]

theorem ordinal.zero_mod (b : ordinal) :

0 % b = 0

theorem ordinal.div_add_mod (a b : ordinal) :

b * (a / b) + a % b = a

theorem ordinal.mod_lt (a : ordinal) {b : ordinal} (h : b ≠ 0) :

a % b < b

@[simp]

theorem ordinal.mod_self (a : ordinal) :

a % a = 0

@[simp]

theorem ordinal.mod_one (a : ordinal) :

a % 1 = 0

theorem ordinal.dvd_of_mod_eq_zero {a b : ordinal} (H : a % b = 0) :

b ∣ a

theorem ordinal.mod_eq_zero_of_dvd {a b : ordinal} (H : b ∣ a) :

a % b = 0

theorem ordinal.dvd_iff_mod_eq_zero {a b : ordinal} :

b ∣ a ↔ a % b = 0

@[simp]

theorem ordinal.mul_add_mod_self (x y z : ordinal) :

(x * y + z) % x = z % x

@[simp]

theorem ordinal.mul_mod (x y : ordinal) :

x * y % x = 0

theorem ordinal.mod_mod_of_dvd (a : ordinal) {b c : ordinal} (h : c ∣ b) :

a % b % c = a % c

@[simp]

theorem ordinal.mod_mod (a b : ordinal) :

a % b % b = a % b

Families of ordinals #

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

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

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

ordinal.bfamily_of_family' r f = λ (a : ordinal) (ha : a < ordinal.type r), f (ordinal.enum r a ha)

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

ordinal.bfamily_of_family = ordinal.bfamily_of_family' well_ordering_rel

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

ordinal.family_of_bfamily' r ho f = λ (i : ι), f (ordinal.typein r i) _

def ordinal.family_of_bfamily {α : Type u_1} (o : ordinal) (f : Π (a : ordinal), a < o → α) :

(quotient.out o).α → α

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

Equations

o.family_of_bfamily f = ordinal.family_of_bfamily' has_lt.lt _ f

@[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

@[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

@[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

@[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

def ordinal.brange {α : Type u_1} (o : ordinal) (f : Π (a : ordinal), a < o → α) :

set α

The range of a family indexed by ordinals.

Equations

o.brange f = {a : α | ∃ (i : ordinal) (hi : i < o), f i hi = a}

theorem ordinal.mem_brange {α : Type u_1} {o : ordinal} {f : Π (a : ordinal), a < o → α} {a : α} :

a ∈ o.brange f ↔ ∃ (i : ordinal) (hi : i < o), f i hi = a

theorem ordinal.mem_brange_self {α : Type u_1} {o : ordinal} (f : Π (a : ordinal), a < o → α) (i : ordinal) (hi : i < o) :

f i hi ∈ o.brange f

@[simp]

theorem ordinal.range_family_of_bfamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [is_well_order ι r] {o : ordinal} (ho : ordinal.type r = o) (f : Π (a : ordinal), a < o → α) :

set.range (ordinal.family_of_bfamily' r ho f) = o.brange f

@[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

@[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

@[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

@[simp]

theorem ordinal.brange_const {α : Type u_1} {o : ordinal} (ho : o ≠ 0) {c : α} :

o.brange (λ (_x : ordinal) (_x : _x < o), c) = {c}

theorem ordinal.comp_bfamily_of_family' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [is_well_order ι r] (f : ι → α) (g : α → β) :

(λ (i : ordinal) (hi : i < ordinal.type r), g (ordinal.bfamily_of_family' r f i hi)) = ordinal.bfamily_of_family' r (g ∘ f)

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)

theorem ordinal.comp_family_of_bfamily' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [is_well_order ι r] {o : ordinal} (ho : ordinal.type r = o) (f : Π (a : ordinal), a < o → α) (g : α → β) :

g ∘ ordinal.family_of_bfamily' r ho f = ordinal.family_of_bfamily' r ho (λ (i : ordinal) (hi : i < o), g (f i hi))

theorem ordinal.comp_family_of_bfamily {α : Type u_1} {β : Type u_2} {o : ordinal} (f : Π (a : ordinal), a < o → α) (g : α → β) :

g ∘ o.family_of_bfamily f = o.family_of_bfamily (λ (i : ordinal) (hi : i < o), g (f i hi))

Supremum of a family of ordinals #

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

The supremum of a family of ordinals

Equations

ordinal.sup f = supr f

@[simp]

theorem ordinal.Sup_eq_sup {ι : Type u} (f : ι → ordinal) :

has_Sup.Sup (set.range f) = ordinal.sup f

theorem ordinal.bdd_above_range {ι : Type u} (f : ι → ordinal) :

bdd_above (set.range f)

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

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

f i ≤ ordinal.sup f

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

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

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

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

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

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

theorem ordinal.ne_sup_iff_lt_sup {ι : Type u_1} {f : ι → ordinal} :

(∀ (i : ι), f i ≠ ordinal.sup f) ↔ ∀ (i : ι), f i < ordinal.sup f

theorem ordinal.sup_not_succ_of_ne_sup {ι : Type u_1} {f : ι → ordinal} (hf : ∀ (i : ι), f i ≠ ordinal.sup f) {a : ordinal} (hao : a < ordinal.sup f) :

order.succ a < ordinal.sup f

@[simp]

theorem ordinal.sup_eq_zero_iff {ι : Type u_1} {f : ι → ordinal} :

ordinal.sup f = 0 ↔ ∀ (i : ι), f i = 0

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

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

@[simp]

theorem ordinal.sup_empty {ι : Type u_1} [is_empty ι] (f : ι → ordinal) :

ordinal.sup f = 0

@[simp]

theorem ordinal.sup_const {ι : Type u_1} [hι : nonempty ι] (o : ordinal) :

ordinal.sup (λ (_x : ι), o) = o

@[simp]

theorem ordinal.sup_unique {ι : Type u_1} [unique ι] (f : ι → ordinal) :

ordinal.sup f = f inhabited.default

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

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

@[simp]

theorem ordinal.sup_sum {α : Type u} {β : Type v} (f : α ⊕ β → ordinal) :

ordinal.sup f = linear_order.max (ordinal.sup (λ (a : α), f (sum.inl a))) (ordinal.sup (λ (b : β), f (sum.inr b)))

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)

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)

@[protected, instance]

def ordinal.small_Iio (o : ordinal) :

small ↥(set.Iio o)

@[protected, instance]

def ordinal.small_Iic (o : ordinal) :

small ↥(set.Iic o)

theorem ordinal.bdd_above_iff_small {s : set ordinal} :

bdd_above s ↔ small ↥s

theorem ordinal.bdd_above_of_small (s : set ordinal) [h : small ↥s] :

theorem ordinal.sup_eq_Sup {s : set ordinal} (hs : small ↥s) :

ordinal.sup (λ (x : shrink ↥s), ↑(⇑((equiv_shrink ↥s).symm) x)) = has_Sup.Sup s

theorem ordinal.Sup_ord {s : set cardinal} (hs : bdd_above s) :

(has_Sup.Sup s).ord = has_Sup.Sup (cardinal.ord '' s)

theorem ordinal.supr_ord {ι : Sort u_1} {f : ι → cardinal} (hf : bdd_above (set.range f)) :

(supr f).ord = ⨆ (i : ι), (f i).ord

theorem ordinal.sup_eq_sup {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [is_well_order ι r] [is_well_order ι' r'] {o : ordinal} (ho : ordinal.type r = o) (ho' : ordinal.type r' = o) (f : Π (a : ordinal), a < o → ordinal) :

ordinal.sup (ordinal.family_of_bfamily' r ho f) = ordinal.sup (ordinal.family_of_bfamily' r' ho' f)

noncomputable def ordinal.bsup (o : ordinal) (f : Π (a : ordinal), a < o → 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

o.bsup f = ordinal.sup (o.family_of_bfamily f)

@[simp]

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

ordinal.sup (o.family_of_bfamily f) = o.bsup f

@[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

@[simp]

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

has_Sup.Sup (o.brange f) = o.bsup f

@[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

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)

@[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

theorem ordinal.bsup_congr {o₁ o₂ : ordinal} (f : Π (a : ordinal), a < o₁ → ordinal) (ho : o₁ = o₂) :

o₁.bsup f = o₂.bsup (λ (a : ordinal) (h : a < o₂), f a _)

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

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

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

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

theorem ordinal.le_bsup {o : ordinal} (f : Π (a : ordinal), a < 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) {a : ordinal} :

a < o.bsup f ↔ ∃ (i : ordinal) (hi : i < o), a < f i hi

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

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 → order.succ a < o.bsup f

@[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

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 → order.succ a < o) (i : ordinal) (h : i < o) :

f i h < o.bsup f

theorem ordinal.bsup_succ_of_mono {o : ordinal} {f : Π (a : ordinal), a < order.succ o → ordinal} (hf : ∀ {i j : ordinal} (hi : i < order.succ o) (hj : j < order.succ o), i ≤ j → f i hi ≤ f j hj) :

(order.succ o).bsup f = f o _

@[simp]

theorem ordinal.bsup_zero (f : Π (a : ordinal), a < 0 → ordinal) :

0.bsup f = 0

theorem ordinal.bsup_const {o : ordinal} (ho : o ≠ 0) (a : ordinal) :

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

@[simp]

theorem ordinal.bsup_one (f : Π (a : ordinal), a < 1 → ordinal) :

1.bsup f = f 0 zero_lt_one

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

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

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

The least strict upper bound of a family of ordinals.

Equations

ordinal.lsub f = ordinal.sup (order.succ ∘ f)

@[simp]

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

ordinal.sup (order.succ ∘ f) = ordinal.lsub f

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

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

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

(∀ (i : ι), f i < a) → ordinal.lsub f ≤ a

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

f i < ordinal.lsub f

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

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

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

ordinal.sup f ≤ ordinal.lsub f

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

ordinal.lsub f ≤ order.succ (ordinal.sup f)

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

ordinal.sup f = ordinal.lsub f ∨ order.succ (ordinal.sup f) = ordinal.lsub f

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

order.succ (ordinal.sup f) ≤ ordinal.lsub f ↔ ∃ (i : ι), f i = ordinal.sup f

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

order.succ (ordinal.sup f) = ordinal.lsub f ↔ ∃ (i : ι), f i = ordinal.sup f

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

ordinal.sup f = ordinal.lsub f ↔ ∀ (a : ordinal), a < ordinal.lsub f → order.succ a < ordinal.lsub f

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

ordinal.sup f = ordinal.lsub f ↔ ∀ (i : ι), f i < ordinal.sup f

@[simp]

theorem ordinal.lsub_empty {ι : Type u_1} [h : is_empty ι] (f : ι → ordinal) :

ordinal.lsub f = 0

theorem ordinal.lsub_pos {ι : Type u_1} [h : nonempty ι] (f : ι → ordinal) :

0 < ordinal.lsub f

@[simp]

theorem ordinal.lsub_eq_zero_iff {ι : Type u_1} {f : ι → ordinal} :

ordinal.lsub f = 0 ↔ is_empty ι

@[simp]

theorem ordinal.lsub_const {ι : Type u_1} [hι : nonempty ι] (o : ordinal) :

ordinal.lsub (λ (_x : ι), o) = order.succ o

@[simp]

theorem ordinal.lsub_unique {ι : Type u_1} [hι : unique ι] (f : ι → ordinal) :

ordinal.lsub f = order.succ (f inhabited.default)

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

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

@[simp]

theorem ordinal.lsub_sum {α : Type u} {β : Type v} (f : α ⊕ β → ordinal) :

ordinal.lsub f = linear_order.max (ordinal.lsub (λ (a : α), f (sum.inl a))) (ordinal.lsub (λ (b : β), f (sum.inr b)))

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

ordinal.lsub f ∉ set.range f

theorem ordinal.nonempty_compl_range {ι : Type u} (f : ι → ordinal) :

(set.range f)ᶜ.nonempty

@[simp]

theorem ordinal.lsub_typein (o : ordinal) :

ordinal.lsub (ordinal.typein has_lt.lt) = o

theorem ordinal.sup_typein_limit {o : ordinal} (ho : ∀ (a : ordinal), a < o → order.succ a < o) :

ordinal.sup (ordinal.typein has_lt.lt) = o

@[simp]

theorem ordinal.sup_typein_succ {o : ordinal} :

ordinal.sup (ordinal.typein has_lt.lt) = o

noncomputable def ordinal.blsub (o : ordinal) (f : Π (a : ordinal), a < o → 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

o.blsub f = o.bsup (λ (a : ordinal) (ha : a < o), order.succ (f a ha))

@[simp]

theorem ordinal.bsup_eq_blsub (o : ordinal) (f : Π (a : ordinal), a < o → ordinal) :

o.bsup (λ (a : ordinal) (ha : a < o), order.succ (f a ha)) = o.blsub f

theorem ordinal.lsub_eq_blsub' {ι : Type u_1} (r : ι → ι → Prop) [is_well_order ι r] {o : ordinal} (ho : ordinal.type r = o) (f : Π (a : ordinal), a < o → ordinal) :

ordinal.lsub (ordinal.family_of_bfamily' r ho f) = o.blsub f

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)

@[simp]

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

ordinal.lsub (o.family_of_bfamily f) = o.blsub f

@[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

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)

@[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

theorem ordinal.blsub_congr {o₁ o₂ : ordinal} (f : Π (a : ordinal), a < o₁ → ordinal) (ho : o₁ = o₂) :

o₁.blsub f = o₂.blsub (λ (a : ordinal) (h : a < o₂), f a _)

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

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

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

(∀ (i : ordinal) (h : i < o), f i h < a) → o.blsub f ≤ a

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

f i h < o.blsub f

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

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

o.bsup f ≤ o.blsub f

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

o.blsub f ≤ order.succ (o.bsup f)

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

o.bsup f = o.blsub f ∨ order.succ (o.bsup f) = o.blsub f

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

order.succ (o.bsup f) ≤ o.blsub f ↔ ∃ (i : ordinal) (hi : i < o), f i hi = o.bsup f

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

order.succ (o.bsup f) = o.blsub f ↔ ∃ (i : ordinal) (hi : i < o), f i hi = o.bsup f

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

o.bsup f = o.blsub f ↔ ∀ (a : ordinal), a < o.blsub f → order.succ a < o.blsub f

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

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 (order.succ a) _) :

o.bsup f = o.blsub f

theorem ordinal.blsub_succ_of_mono {o : ordinal} {f : Π (a : ordinal), a < order.succ o → ordinal} (hf : ∀ {i j : ordinal} (hi : i < order.succ o) (hj : j < order.succ o), i ≤ j → f i hi ≤ f j hj) :

(order.succ o).blsub f = order.succ (f o _)

@[simp]

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

o.blsub f = 0 ↔ o = 0

@[simp]

theorem ordinal.blsub_zero (f : Π (a : ordinal), a < 0 → ordinal) :

0.blsub f = 0

theorem ordinal.blsub_pos {o : ordinal} (ho : 0 < o) (f : Π (a : ordinal), a < o → ordinal) :

0 < o.blsub f

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

theorem ordinal.blsub_const {o : ordinal} (ho : o ≠ 0) (a : ordinal) :

o.blsub (λ (_x : ordinal) (_x : _x < o), a) = order.succ a

@[simp]

theorem ordinal.blsub_one (f : Π (a : ordinal), a < 1 → ordinal) :

1.blsub f = order.succ (f 0 zero_lt_one)

@[simp]

theorem ordinal.blsub_id (o : ordinal) :

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

theorem ordinal.bsup_id_limit {o : ordinal} :

(∀ (a : ordinal), a < o → order.succ a < o) → o.bsup (λ (x : ordinal) (_x : x < o), x) = o

@[simp]

theorem ordinal.bsup_id_succ (o : ordinal) :

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

theorem ordinal.blsub_le_of_brange_subset {o : ordinal} {o' : ordinal} {f : Π (a : ordinal), a < o → ordinal} {g : Π (a : ordinal), a < o' → ordinal} (h : o.brange f ⊆ o'.brange g) :

o.blsub f ≤ o'.blsub g

theorem ordinal.blsub_eq_of_brange_eq {o : ordinal} {o' : ordinal} {f : Π (a : ordinal), a < 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

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

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

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

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

theorem ordinal.is_normal_iff_lt_succ_and_bsup_eq {f : ordinal → ordinal} :

ordinal.is_normal f ↔ (∀ (a : ordinal), f a < f (order.succ a)) ∧ ∀ (o : ordinal), o.is_limit → o.bsup (λ (x : ordinal) (_x : x < o), f x) = f o

theorem ordinal.is_normal_iff_lt_succ_and_blsub_eq {f : ordinal → ordinal} :

ordinal.is_normal f ↔ (∀ (a : ordinal), f a < f (order.succ a)) ∧ ∀ (o : ordinal), o.is_limit → o.blsub (λ (x : ordinal) (_x : x < o), f x) = f o

theorem ordinal.is_normal.eq_iff_zero_and_succ {f g : ordinal → ordinal} (hf : ordinal.is_normal f) (hg : ordinal.is_normal g) :

f = g ↔ f 0 = g 0 ∧ ∀ (a : ordinal), f a = g a → f (order.succ a) = g (order.succ a)

noncomputable def ordinal.blsub₂ (o₁ : ordinal) (o₂ : ordinal) (op : Π (a : ordinal), a < o₁ → Π (b : ordinal), b < o₂ → ordinal) :

A two-argument version of ordinal.blsub.

We don't develop a full API for this, since it's only used in a handful of existence results.

Equations

o₁.blsub₂ o₂ op = ordinal.lsub (λ (x : (quotient.out o₁).α × (quotient.out o₂).α), op (ordinal.typein has_lt.lt x.fst) _ (ordinal.typein has_lt.lt x.snd) _)

theorem ordinal.lt_blsub₂ {o₁ : ordinal} {o₂ : ordinal} (op : Π (a : ordinal), a < o₁ → Π (b : ordinal), b < o₂ → ordinal) {a : ordinal} {b : ordinal} (ha : a < o₁) (hb : b < o₂) :

op a ha b hb < o₁.blsub₂ o₂ op

Minimum excluded ordinals #

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

The minimum excluded ordinal in a family of ordinals.

Equations

ordinal.mex f = has_Inf.Inf (set.range f)ᶜ

theorem ordinal.mex_not_mem_range {ι : Type u} (f : ι → ordinal) :

ordinal.mex f ∉ set.range f

theorem ordinal.le_mex_of_forall {ι : Type u} {f : ι → ordinal} {a : ordinal} (H : ∀ (b : ordinal), b < a → (∃ (i : ι), f i = b)) :

a ≤ ordinal.mex f

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

f i ≠ ordinal.mex f

theorem ordinal.mex_le_of_ne {ι : Type u_1} {f : ι → ordinal} {a : ordinal} (ha : ∀ (i : ι), f i ≠ a) :

ordinal.mex f ≤ a

theorem ordinal.exists_of_lt_mex {ι : Type u_1} {f : ι → ordinal} {a : ordinal} (ha : a < ordinal.mex f) :

∃ (i : ι), f i = a

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

ordinal.mex f ≤ ordinal.lsub f

theorem ordinal.mex_monotone {α β : Type u_1} {f : α → ordinal} {g : β → ordinal} (h : set.range f ⊆ set.range g) :

ordinal.mex f ≤ ordinal.mex g

theorem ordinal.mex_lt_ord_succ_mk {ι : Type (max u_1 u_2)} (f : ι → ordinal) :

ordinal.mex f < (order.succ (cardinal.mk ι)).ord

noncomputable def ordinal.bmex (o : ordinal) (f : Π (a : ordinal), a < o → 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

o.bmex f = ordinal.mex (o.family_of_bfamily f)

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

o.bmex f ∉ o.brange f

theorem ordinal.le_bmex_of_forall {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) {a : ordinal} (H : ∀ (b : ordinal), b < a → (∃ (i : ordinal) (hi : i < o), f i hi = b)) :

a ≤ o.bmex f

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

f i hi ≠ o.bmex f

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

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

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

o.bmex f ≤ o.blsub f

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

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

o.bmex f < (order.succ o.card).ord

Results about injectivity and surjectivity #

theorem not_surjective_of_ordinal {α : Type u} (f : α → ordinal) :

¬function.surjective f

theorem not_injective_of_ordinal {α : Type u} (f : ordinal → α) :

¬function.injective f

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

¬function.surjective f

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

¬function.injective f

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 #

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

ordinal → ordinal

Enumerator function for an unbounded set of ordinals.

Equations

ordinal.enum_ord S = ordinal.lt_wf.fix (λ (o : ordinal) (f : Π (y : ordinal), y < o → ordinal), has_Inf.Inf (S ∩ set.Ici (o.blsub f)))

theorem ordinal.enum_ord_def' {S : set ordinal} (o : ordinal) :

ordinal.enum_ord S o = has_Inf.Inf (S ∩ set.Ici (o.blsub (λ (a : ordinal) (_x : a < o), ordinal.enum_ord S a)))

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

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.

theorem ordinal.enum_ord_mem {S : set ordinal} (hS : set.unbounded has_lt.lt S) (o : ordinal) :

ordinal.enum_ord S o ∈ S

theorem ordinal.blsub_le_enum_ord {S : set ordinal} (hS : set.unbounded has_lt.lt S) (o : ordinal) :

o.blsub (λ (c : ordinal) (_x : c < o), ordinal.enum_ord S c) ≤ ordinal.enum_ord S o

theorem ordinal.enum_ord_strict_mono {S : set ordinal} (hS : set.unbounded has_lt.lt S) :

strict_mono (ordinal.enum_ord S)

theorem ordinal.enum_ord_def {S : set ordinal} (o : ordinal) :

ordinal.enum_ord S o = has_Inf.Inf (S ∩ {b : ordinal | ∀ (c : ordinal), c < o → ordinal.enum_ord S c < b})

A more workable definition for enum_ord.

theorem ordinal.enum_ord_def_nonempty {S : set ordinal} (hS : set.unbounded has_lt.lt S) {o : ordinal} :

{x : ordinal | x ∈ S ∧ ∀ (c : ordinal), c < o → ordinal.enum_ord S c < x}.nonempty

The set in enum_ord_def is nonempty.

@[simp]

theorem ordinal.enum_ord_range {f : ordinal → ordinal} (hf : strict_mono f) :

ordinal.enum_ord (set.range f) = f

@[simp]

theorem ordinal.enum_ord_univ :

ordinal.enum_ord set.univ = id

@[simp]

theorem ordinal.enum_ord_zero {S : set ordinal} :

ordinal.enum_ord S 0 = has_Inf.Inf S

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 (order.succ b) ≤ a

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

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

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

ordinal.enum_ord_order_iso hS = strict_mono.order_iso_of_surjective (λ (o : ordinal), ⟨ordinal.enum_ord S o, _⟩) _ _

theorem ordinal.range_enum_ord {S : set ordinal} (hS : set.unbounded has_lt.lt S) :

set.range (ordinal.enum_ord S) = S

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.

Casting naturals into ordinals, compatibility with operations #

@[simp]

theorem ordinal.one_add_nat_cast (m : ℕ) :

1 + ↑m = order.succ ↑m

@[simp, norm_cast]

theorem ordinal.nat_cast_mul (m n : ℕ) :

↑(m * n) = ↑m * ↑n

@[simp, norm_cast]

theorem ordinal.nat_cast_le {m n : ℕ} :

↑m ≤ ↑n ↔ m ≤ n

@[simp, norm_cast]

theorem ordinal.nat_cast_lt {m n : ℕ} :

↑m < ↑n ↔ m < n

@[simp, norm_cast]

theorem ordinal.nat_cast_inj {m n : ℕ} :

↑m = ↑n ↔ m = n

@[simp, norm_cast]

theorem ordinal.nat_cast_eq_zero {n : ℕ} :

↑n = 0 ↔ n = 0

theorem ordinal.nat_cast_ne_zero {n : ℕ} :

↑n ≠ 0 ↔ n ≠ 0

@[simp, norm_cast]

theorem ordinal.nat_cast_pos {n : ℕ} :

0 < ↑n ↔ 0 < n

@[simp, norm_cast]

theorem ordinal.nat_cast_sub (m n : ℕ) :

↑(m - n) = ↑m - ↑n

@[simp, norm_cast]

theorem ordinal.nat_cast_div (m n : ℕ) :

↑(m / n) = ↑m / ↑n

@[simp, norm_cast]

theorem ordinal.nat_cast_mod (m n : ℕ) :

↑(m % n) = ↑m % ↑n

@[simp]

theorem ordinal.lift_nat_cast (n : ℕ) :

↑n.lift = ↑n

Properties of `omega` #

@[simp]

theorem cardinal.ord_aleph_0 :

cardinal.aleph_0.ord = ordinal.omega

@[simp]

theorem cardinal.add_one_of_aleph_0_le {c : cardinal} (h : cardinal.aleph_0 ≤ c) :

c + 1 = c

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

a < b + c ↔ ∃ (c' : ordinal) (H : c' < c), a < b + c'

theorem ordinal.lt_omega {o : ordinal} :

o < ordinal.omega ↔ ∃ (n : ℕ), o = ↑n

theorem ordinal.nat_lt_omega (n : ℕ) :

↑n < ordinal.omega

theorem ordinal.omega_pos :

0 < ordinal.omega

theorem ordinal.omega_ne_zero :

ordinal.omega ≠ 0

theorem ordinal.one_lt_omega :

1 < ordinal.omega

theorem ordinal.omega_is_limit :

ordinal.omega.is_limit

theorem ordinal.omega_le {o : ordinal} :

ordinal.omega ≤ o ↔ ∀ (n : ℕ), ↑n ≤ o

@[simp]

theorem ordinal.sup_nat_cast :

ordinal.sup nat.cast = ordinal.omega

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

ordinal.omega ≤ o

theorem ordinal.is_limit_iff_omega_dvd {a : ordinal} :

a.is_limit ↔ a ≠ 0 ∧ ordinal.omega ∣ 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) * order.succ c' = a * order.succ c' + b) :

(a + b) * c = a * c

theorem ordinal.add_mul_succ {a b : ordinal} (c : ordinal) (ba : b + a = a) :

(a + b) * order.succ c = a * order.succ c + b

theorem ordinal.add_mul_limit {a b c : ordinal} (ba : b + a = a) (l : c.is_limit) :

(a + b) * c = a * c

theorem ordinal.add_le_of_forall_add_lt {a b c : ordinal} (hb : 0 < b) (h : ∀ (d : ordinal), d < b → a + d < c) :

a + b ≤ c

theorem ordinal.is_normal.apply_omega {f : ordinal → ordinal} (hf : ordinal.is_normal f) :

ordinal.sup (f ∘ nat.cast) = f ordinal.omega

@[simp]

theorem ordinal.sup_add_nat (o : ordinal) :

ordinal.sup (λ (n : ℕ), o + ↑n) = o + ordinal.omega

@[simp]

theorem ordinal.sup_mul_nat (o : ordinal) :

ordinal.sup (λ (n : ℕ), o * ↑n) = o * ordinal.omega

noncomputable def acc.rank {α : Type u} {r : α → α → Prop} {a : α} (h : acc r a) :

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

Equations

h.rank = h.rec_on (λ (a : α) (h : ∀ (y : α), r y a → acc r y) (ih : Π (y : α), r y a → ordinal), ordinal.sup (λ (b : {b // r b a}), order.succ (ih ↑b _)))

theorem acc.rank_eq {α : Type u} {r : α → α → Prop} {a : α} (h : acc r a) :

h.rank = ordinal.sup (λ (b : {b // r b a}), order.succ _.rank)

theorem acc.rank_lt_of_rel {α : Type u} {r : α → α → Prop} {a b : α} (hb : acc r b) (h : r a b) :

_.rank < hb.rank

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

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

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

Equations

hwf.rank a = _.rank

theorem well_founded.rank_eq {α : Type u} {r : α → α → Prop} {a : α} (hwf : well_founded r) :

hwf.rank a = ordinal.sup (λ (b : {b // r b a}), order.succ (hwf.rank ↑b))

theorem well_founded.rank_lt_of_rel {α : Type u} {r : α → α → Prop} {a b : α} (hwf : well_founded r) (h : r a b) :

hwf.rank a < hwf.rank b

theorem well_founded.rank_strict_mono {α : Type u} [preorder α] [well_founded_lt α] :

strict_mono is_well_founded.wf.rank

theorem well_founded.rank_strict_anti {α : Type u} [preorder α] [well_founded_gt α] :

strict_anti is_well_founded.wf.rank