Ordinal arithmetic

Ordinals have an addition (corresponding to disjoint union) that turns them into an additive monoid, and a multiplication (corresponding to the lexicographic order on the product) that turns them into a monoid. One can also define correspondingly a subtraction, a division, a successor function, a power function and a logarithm function.

We also define limit ordinals and prove the basic induction principle on ordinals separating successor ordinals and limit ordinals, in limitRecOn.

Main definitions and results

• o₁ + o₂ is the order on the disjoint union of o₁ and o₂ obtained by declaring that every element of o₁ is smaller than every element of o₂.
• o₁ - o₂ is the unique ordinal o such that o₂ + o = o₁, when o₂ ≤ o₁.
• o₁ * o₂ is the lexicographic order on o₂ × o₁.
• o₁ / o₂ is the ordinal o such that o₁ = o₂ * o + o' with o' < o₂. We also define the divisibility predicate, and a modulo operation.
• Order.succ o = o + 1 is the successor of o.
• pred o if the predecessor of o. If o is not a successor, we set pred o = o.

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

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

• IsLimit o: an ordinal is a limit ordinal if it is neither 0 nor a successor.
• limitRecOn is the main induction principle of ordinals: if one can prove a property by induction at successor ordinals and at limit ordinals, then it holds for all ordinals.
• IsNormal: a function f : Ordinal → Ordinal satisfies IsNormal if it is strictly increasing and order-continuous, i.e., the image f o of a limit ordinal o is the sup of f a for a < o.
• 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 : Ordinal.{v}) (b : Ordinal.{v}) : Ordinal.lift.{u, v} (a + b) = Ordinal.lift.{u, v} a + Ordinal.lift.{u, v} b

@[simp]

theorem Ordinal.lift_succ (a : Ordinal.{v}) : Ordinal.lift.{u, v} (Order.succ a) = Order.succ (Ordinal.lift.{u, v} a)

instance Ordinal.instAddLeftReflectLE : AddLeftReflectLE Ordinal.{u}

Equations

• Ordinal.instAddLeftReflectLE = ⋯

theorem Ordinal.add_left_cancel (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} : a + b = a + c ↔ b = c

instance Ordinal.instAddLeftStrictMono : AddLeftStrictMono Ordinal.{u}

Equations

• Ordinal.instAddLeftStrictMono = ⋯

instance Ordinal.instAddLeftReflectLT : AddLeftReflectLT Ordinal.{u}

Equations

• Ordinal.instAddLeftReflectLT = ⋯

instance Ordinal.instAddRightReflectLT : AddRightReflectLT Ordinal.{u}

Equations

• Ordinal.instAddRightReflectLT = ⋯

theorem Ordinal.add_le_add_iff_right {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (n : ℕ) : a + ↑n ≤ b + ↑n ↔ a ≤ b

theorem Ordinal.add_right_cancel {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (n : ℕ) : a + ↑n = b + ↑n ↔ a = b

theorem Ordinal.add_eq_zero_iff {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} : a + b = 0 ↔ a = 0 ∧ b = 0

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

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

The predecessor of an ordinal

def Ordinal.pred (o : Ordinal.{u_4}) : Ordinal.{u_4}

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

Equations

• o.pred = if h : ∃ (a : Ordinal.{?u.2}), o = Order.succ a then Classical.choose h else o

@[simp]

theorem Ordinal.pred_succ (o : Ordinal.{u_4}) : (Order.succ o).pred = o

theorem Ordinal.pred_le_self (o : Ordinal.{u_4}) : o.pred ≤ o

theorem Ordinal.pred_eq_iff_not_succ {o : Ordinal.{u_4}} : o.pred = o ↔ ¬∃ (a : Ordinal.{u_4}), o = Order.succ a

theorem Ordinal.pred_eq_iff_not_succ' {o : Ordinal.{u_4}} : o.pred = o ↔ ∀ (a : Ordinal.{u_4}), o ≠ Order.succ a

theorem Ordinal.pred_lt_iff_is_succ {o : Ordinal.{u_4}} : o.pred < o ↔ ∃ (a : Ordinal.{u_4}), o = Order.succ a

@[simp]

theorem Ordinal.pred_zero : Ordinal.pred 0 = 0

theorem Ordinal.succ_pred_iff_is_succ {o : Ordinal.{u_4}} : Order.succ o.pred = o ↔ ∃ (a : Ordinal.{u_4}), o = Order.succ a

theorem Ordinal.succ_lt_of_not_succ {o : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : ¬∃ (a : Ordinal.{u_4}), o = Order.succ a) : Order.succ b < o ↔ b < o

theorem Ordinal.lt_pred {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} : a < b.pred ↔ Order.succ a < b

theorem Ordinal.pred_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} : a.pred ≤ b ↔ a ≤ Order.succ b

@[simp]

theorem Ordinal.lift_is_succ {o : Ordinal.{v}} : (∃ (a : Ordinal.{max v u} ), Ordinal.lift.{u, v} o = Order.succ a) ↔ ∃ (a : Ordinal.{v}), o = Order.succ a

@[simp]

theorem Ordinal.lift_pred (o : Ordinal.{v}) : Ordinal.lift.{u, v} o.pred = (Ordinal.lift.{u, v} o).pred

Limit ordinals

def Ordinal.IsLimit (o : Ordinal.{u_4}) : Prop

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

TODO: deprecate this in favor of Order.IsSuccLimit.

Equations

• o.IsLimit = (o ≠ 0 ∧ ∀ a < o, Order.succ a < o)

theorem Ordinal.IsLimit.isSuccPrelimit {o : Ordinal.{u_4}} (h : o.IsLimit) : Order.IsSuccPrelimit o

@[deprecated Ordinal.IsLimit.isSuccPrelimit]

theorem Ordinal.IsLimit.isSuccLimit {o : Ordinal.{u_4}} (h : o.IsLimit) : Order.IsSuccPrelimit o

Alias of Ordinal.IsLimit.isSuccPrelimit.

theorem Ordinal.IsLimit.succ_lt {o : Ordinal.{u_4}} {a : Ordinal.{u_4}} (h : o.IsLimit) : a < o → Order.succ a < o

theorem Ordinal.isSuccPrelimit_zero : Order.IsSuccPrelimit 0

@[deprecated Ordinal.isSuccPrelimit_zero]

theorem Ordinal.isSuccLimit_zero : Order.IsSuccPrelimit 0

Alias of Ordinal.isSuccPrelimit_zero.

theorem Ordinal.not_zero_isLimit : ¬Ordinal.IsLimit 0

theorem Ordinal.not_succ_isLimit (o : Ordinal.{u_4}) : ¬(Order.succ o).IsLimit

theorem Ordinal.not_succ_of_isLimit {o : Ordinal.{u_4}} (h : o.IsLimit) : ¬∃ (a : Ordinal.{u_4}), o = Order.succ a

theorem Ordinal.succ_lt_of_isLimit {o : Ordinal.{u_4}} {a : Ordinal.{u_4}} (h : o.IsLimit) : Order.succ a < o ↔ a < o

theorem Ordinal.le_succ_of_isLimit {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_4}} : o ≤ Order.succ a ↔ o ≤ a

theorem Ordinal.limit_le {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_4}} : o ≤ a ↔ ∀ x < o, x ≤ a

theorem Ordinal.lt_limit {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_4}} : a < o ↔ ∃ x < o, a < x

@[simp]

theorem Ordinal.lift_isLimit (o : Ordinal.{v}) : (Ordinal.lift.{u, v} o).IsLimit ↔ o.IsLimit

theorem Ordinal.IsLimit.pos {o : Ordinal.{u_4}} (h : o.IsLimit) : 0 < o

theorem Ordinal.IsLimit.one_lt {o : Ordinal.{u_4}} (h : o.IsLimit) : 1 < o

theorem Ordinal.IsLimit.nat_lt {o : Ordinal.{u_4}} (h : o.IsLimit) (n : ℕ) : ↑n < o

theorem Ordinal.zero_or_succ_or_limit (o : Ordinal.{u_4}) : o = 0 ∨ (∃ (a : Ordinal.{u_4}), o = Order.succ a) ∨ o.IsLimit

theorem Ordinal.isLimit_of_not_succ_of_ne_zero {o : Ordinal.{u_4}} (h : ¬∃ (a : Ordinal.{u_4}), o = Order.succ a) (h' : o ≠ 0) : o.IsLimit

theorem Ordinal.IsLimit.sSup_Iio {o : Ordinal.{u_4}} (h : o.IsLimit) : sSup (Set.Iio o) = o

theorem Ordinal.IsLimit.iSup_Iio {o : Ordinal.{u_4}} (h : o.IsLimit) : ⨆ (a : ↑(Set.Iio o)), ↑a = o

def Ordinal.limitRecOn {C : Ordinal.{u_5} → Sort u_4} (o : Ordinal.{u_5}) (H₁ : C 0) (H₂ : (o : Ordinal.{u_5}) → C o → C (Order.succ o)) (H₃ : (o : Ordinal.{u_5}) → o.IsLimit → ((o' : Ordinal.{u_5}) → 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ordinal.limitRecOn_zero {C : Ordinal.{u_4} → Sort u_5} (H₁ : C 0) (H₂ : (o : Ordinal.{u_4}) → C o → C (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → C o') → C o) : Ordinal.limitRecOn 0 H₁ H₂ H₃ = H₁

@[simp]

theorem Ordinal.limitRecOn_succ {C : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : C 0) (H₂ : (o : Ordinal.{u_4}) → C o → C (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → C o') → C o) : (Order.succ o).limitRecOn H₁ H₂ H₃ = H₂ o (o.limitRecOn H₁ H₂ H₃)

@[simp]

theorem Ordinal.limitRecOn_limit {C : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : C 0) (H₂ : (o : Ordinal.{u_4}) → C o → C (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → C o') → C o) (h : o.IsLimit) : o.limitRecOn H₁ H₂ H₃ = H₃ o h fun (x : Ordinal.{u_4}) (_h : x < o) => x.limitRecOn H₁ H₂ H₃

def Ordinal.boundedLimitRecOn {l : Ordinal.{u_5}} (lLim : l.IsLimit) {C : ↑(Set.Iio l) → Sort u_4} (o : ↑(Set.Iio l)) (H₁ : C ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → C o → C ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → (↑o).IsLimit → ((o' : ↑(Set.Iio l)) → o' < o → C o') → C o) : C o

Bounded recursion on ordinals. Similar to limitRecOn, with the assumption o < l added to all cases. The final term's domain is the ordinals below l.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ordinal.boundedLimitRec_zero {l : Ordinal.{u_4}} (lLim : l.IsLimit) {C : ↑(Set.Iio l) → Sort u_5} (H₁ : C ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → C o → C ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → (↑o).IsLimit → ((o' : ↑(Set.Iio l)) → o' < o → C o') → C o) : Ordinal.boundedLimitRecOn lLim ⟨0, ⋯⟩ H₁ H₂ H₃ = H₁

@[simp]

theorem Ordinal.boundedLimitRec_succ {l : Ordinal.{u_4}} (lLim : l.IsLimit) {C : ↑(Set.Iio l) → Sort u_5} (o : ↑(Set.Iio l)) (H₁ : C ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → C o → C ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → (↑o).IsLimit → ((o' : ↑(Set.Iio l)) → o' < o → C o') → C o) : Ordinal.boundedLimitRecOn lLim ⟨Order.succ ↑o, ⋯⟩ H₁ H₂ H₃ = H₂ o (Ordinal.boundedLimitRecOn lLim o H₁ H₂ H₃)

theorem Ordinal.boundedLimitRec_limit {l : Ordinal.{u_4}} (lLim : l.IsLimit) {C : ↑(Set.Iio l) → Sort u_5} (o : ↑(Set.Iio l)) (H₁ : C ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → C o → C ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → (↑o).IsLimit → ((o' : ↑(Set.Iio l)) → o' < o → C o') → C o) (oLim : (↑o).IsLimit) : Ordinal.boundedLimitRecOn lLim o H₁ H₂ H₃ = H₃ o oLim fun (x : ↑(Set.Iio l)) (x_1 : x < o) => Ordinal.boundedLimitRecOn lLim x H₁ H₂ H₃

instance Ordinal.orderTopToTypeSucc (o : Ordinal.{u_4}) : OrderTop (Order.succ o).toType

Equations

• o.orderTopToTypeSucc = OrderTop.mk ⋯

theorem Ordinal.enum_succ_eq_top {o : Ordinal.{u_4}} : (Ordinal.enum fun (x1 x2 : (Order.succ o).toType) => x1 < x2) ⟨o, ⋯⟩ = ⊤

theorem Ordinal.has_succ_of_type_succ_lt {α : Type u_4} {r : α → α → Prop} [wo : IsWellOrder α r] (h : ∀ a < Ordinal.type r, Order.succ a < Ordinal.type r) (x : α) : ∃ (y : α), r x y

theorem Ordinal.toType_noMax_of_succ_lt {o : Ordinal.{u_4}} (ho : ∀ a < o, Order.succ a < o) : NoMaxOrder o.toType

@[deprecated Ordinal.toType_noMax_of_succ_lt]

theorem Ordinal.out_no_max_of_succ_lt {o : Ordinal.{u_4}} (ho : ∀ a < o, Order.succ a < o) : NoMaxOrder o.toType

Alias of Ordinal.toType_noMax_of_succ_lt.

theorem Ordinal.bounded_singleton {α : Type u_1} {r : α → α → Prop} [IsWellOrder α r] (hr : (Ordinal.type r).IsLimit) (x : α) : Set.Bounded r {x}

@[simp]

theorem Ordinal.typein_ordinal (o : Ordinal.{u}) : (Ordinal.typein fun (x1 x2 : Ordinal.{u}) => x1 < x2).toRelEmbedding o = Ordinal.lift.{u + 1, u} o

@[deprecated Ordinal.typein_ordinal]

theorem Ordinal.type_subrel_lt (o : Ordinal.{u}) : Ordinal.type (Subrel (fun (x1 x2 : Ordinal.{u}) => x1 < x2) {o' : Ordinal.{u} | o' < o}) = Ordinal.lift.{u + 1, u} o

theorem Ordinal.mk_Iio_ordinal (o : Ordinal.{u}) : Cardinal.mk ↑(Set.Iio o) = Cardinal.lift.{u + 1, u} o.card

@[deprecated Ordinal.mk_Iio_ordinal]

theorem Ordinal.mk_initialSeg (o : Ordinal.{u}) : Cardinal.mk ↑{o' : Ordinal.{u} | o' < o} = Cardinal.lift.{u + 1, u} o.card

Normal ordinal functions

def Ordinal.IsNormal (f : Ordinal.{u_4} → Ordinal.{u_5}) : 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.IsNormal f = ((∀ (o : Ordinal.{?u.21}), f o < f (Order.succ o)) ∧ ∀ (o : Ordinal.{?u.21}), o.IsLimit → ∀ (a : Ordinal.{?u.20}), f o ≤ a ↔ ∀ b < o, f b ≤ a)

theorem Ordinal.IsNormal.limit_le {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) {o : Ordinal.{u_4}} : o.IsLimit → ∀ {a : Ordinal.{u_5}}, f o ≤ a ↔ ∀ b < o, f b ≤ a

theorem Ordinal.IsNormal.limit_lt {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_5}} : a < f o ↔ ∃ b < o, a < f b

theorem Ordinal.IsNormal.strictMono {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) : StrictMono f

theorem Ordinal.IsNormal.monotone {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) : Monotone f

theorem Ordinal.isNormal_iff_strictMono_limit (f : Ordinal.{u_4} → Ordinal.{u_5}) : Ordinal.IsNormal f ↔ StrictMono f ∧ ∀ (o : Ordinal.{u_4}), o.IsLimit → ∀ (a : Ordinal.{u_5}), (∀ b < o, f b ≤ a) → f o ≤ a

theorem Ordinal.IsNormal.lt_iff {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} : f a < f b ↔ a < b

theorem Ordinal.IsNormal.le_iff {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} : f a ≤ f b ↔ a ≤ b

theorem Ordinal.IsNormal.inj {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} : f a = f b ↔ a = b

theorem Ordinal.IsNormal.id_le {f : Ordinal.{u_4} → Ordinal.{u_4}} (H : Ordinal.IsNormal f) : id ≤ f

theorem Ordinal.IsNormal.le_apply {f : Ordinal.{u_4} → Ordinal.{u_4}} (H : Ordinal.IsNormal f) {a : Ordinal.{u_4}} : a ≤ f a

@[deprecated Ordinal.IsNormal.le_apply]

theorem Ordinal.IsNormal.self_le {f : Ordinal.{u_4} → Ordinal.{u_4}} (H : Ordinal.IsNormal f) (a : Ordinal.{u_4}) : a ≤ f a

theorem Ordinal.IsNormal.le_iff_eq {f : Ordinal.{u_4} → Ordinal.{u_4}} (H : Ordinal.IsNormal f) {a : Ordinal.{u_4}} : f a ≤ a ↔ f a = a

theorem Ordinal.IsNormal.le_set {f : Ordinal.{u_4} → Ordinal.{u_5}} {o : Ordinal.{u_5}} (H : Ordinal.IsNormal f) (p : Set Ordinal.{u_4}) (p0 : p.Nonempty) (b : Ordinal.{u_4}) (H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, a ≤ o) : f b ≤ o ↔ ∀ a ∈ p, f a ≤ o

theorem Ordinal.IsNormal.le_set' {α : Type u_1} {f : Ordinal.{u_4} → Ordinal.{u_5}} {o : Ordinal.{u_5}} (H : Ordinal.IsNormal f) (p : Set α) (p0 : p.Nonempty) (g : α → Ordinal.{u_4}) (b : Ordinal.{u_4}) (H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, g a ≤ o) : f b ≤ o ↔ ∀ a ∈ p, f (g a) ≤ o

theorem Ordinal.IsNormal.refl : Ordinal.IsNormal id

theorem Ordinal.IsNormal.trans {f : Ordinal.{u_4} → Ordinal.{u_5}} {g : Ordinal.{u_6} → Ordinal.{u_4}} (H₁ : Ordinal.IsNormal f) (H₂ : Ordinal.IsNormal g) : Ordinal.IsNormal (f ∘ g)

theorem Ordinal.IsNormal.isLimit {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) {o : Ordinal.{u_4}} (l : o.IsLimit) : (f o).IsLimit

theorem Ordinal.add_le_of_limit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : b.IsLimit) : a + b ≤ c ↔ ∀ b' < b, a + b' ≤ c

theorem Ordinal.isNormal_add_right (a : Ordinal.{u_4}) : Ordinal.IsNormal fun (x : Ordinal.{u_4}) => a + x

@[deprecated Ordinal.isNormal_add_right]

theorem Ordinal.add_isNormal (a : Ordinal.{u_4}) : Ordinal.IsNormal fun (x : Ordinal.{u_4}) => a + x

Alias of Ordinal.isNormal_add_right.

theorem Ordinal.isLimit_add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} : b.IsLimit → (a + b).IsLimit

@[deprecated Ordinal.isLimit_add]

theorem Ordinal.add_isLimit (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} : b.IsLimit → (a + b).IsLimit

Alias of Ordinal.isLimit_add.

theorem Ordinal.IsLimit.add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} : b.IsLimit → (a + b).IsLimit

Alias of Ordinal.isLimit_add.

---

Alias of Ordinal.isLimit_add.

Subtraction on ordinals

instance Ordinal.sub : Sub Ordinal.{u_4}

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

Equations

• Ordinal.sub = { sub := fun (a b : Ordinal.{?u.6}) => sInf {o : Ordinal.{?u.6} | a ≤ b + o} }

theorem Ordinal.le_add_sub (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) : a ≤ b + (a - b)

theorem Ordinal.sub_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} : a - b ≤ c ↔ a ≤ b + c

theorem Ordinal.lt_sub {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} : a < b - c ↔ c + a < b

theorem Ordinal.add_sub_cancel (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) : a + b - a = b

theorem Ordinal.sub_eq_of_add_eq {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : a + b = c) : c - a = b

theorem Ordinal.sub_le_self (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) : a - b ≤ a

theorem Ordinal.add_sub_cancel_of_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : b ≤ a) : b + (a - b) = a

theorem Ordinal.le_sub_of_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : b ≤ a) : c ≤ a - b ↔ b + c ≤ a

theorem Ordinal.sub_lt_of_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : b ≤ a) : a - b < c ↔ a < b + c

instance Ordinal.existsAddOfLE : ExistsAddOfLE Ordinal.{u_4}

Equations

• Ordinal.existsAddOfLE = ⋯

@[simp]

theorem Ordinal.sub_zero (a : Ordinal.{u_4}) : a - 0 = a

@[simp]

theorem Ordinal.zero_sub (a : Ordinal.{u_4}) : 0 - a = 0

@[simp]

theorem Ordinal.sub_self (a : Ordinal.{u_4}) : a - a = 0

theorem Ordinal.sub_eq_zero_iff_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} : a - b = 0 ↔ a ≤ b

theorem Ordinal.sub_sub (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) (c : Ordinal.{u_4}) : a - b - c = a - (b + c)

@[simp]

theorem Ordinal.add_sub_add_cancel (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) (c : Ordinal.{u_4}) : a + b - (a + c) = b - c

theorem Ordinal.isLimit_sub {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (l : a.IsLimit) (h : b < a) : (a - b).IsLimit

@[deprecated Ordinal.isLimit_sub]

theorem Ordinal.sub_isLimit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (l : a.IsLimit) (h : b < a) : (a - b).IsLimit

Alias of Ordinal.isLimit_sub.

theorem Ordinal.one_add_omega0 : 1 + Ordinal.omega0 = Ordinal.omega0

@[deprecated Ordinal.one_add_omega0]

theorem Ordinal.one_add_omega : 1 + Ordinal.omega0 = Ordinal.omega0

Alias of Ordinal.one_add_omega0.

@[simp]

theorem Ordinal.one_add_of_omega0_le {o : Ordinal.{u_4}} (h : Ordinal.omega0 ≤ o) : 1 + o = o

@[deprecated Ordinal.one_add_of_omega0_le]

theorem Ordinal.one_add_of_omega_le {o : Ordinal.{u_4}} (h : Ordinal.omega0 ≤ o) : 1 + o = o

Alias of Ordinal.one_add_of_omega0_le.

Multiplication of ordinals

instance Ordinal.monoid : Monoid Ordinal.{u}

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

Equations

• Ordinal.monoid = Monoid.mk Ordinal.monoid.proof_4 Ordinal.monoid.proof_5 npowRecAuto Ordinal.monoid.proof_8 Ordinal.monoid.proof_9

@[simp]

theorem Ordinal.type_prod_lex {α : Type u} {β : Type u} (r : α → α → Prop) (s : β → β → Prop) [IsWellOrder α r] [IsWellOrder β s] : Ordinal.type (Prod.Lex s r) = Ordinal.type r * Ordinal.type s

instance Ordinal.monoidWithZero : MonoidWithZero Ordinal.{u_4}

Equations

• Ordinal.monoidWithZero = MonoidWithZero.mk Ordinal.monoidWithZero.proof_1 Ordinal.monoidWithZero.proof_2

instance Ordinal.noZeroDivisors : NoZeroDivisors Ordinal.{u_4}

Equations

• Ordinal.noZeroDivisors = ⋯

@[simp]

theorem Ordinal.lift_mul (a : Ordinal.{v}) (b : Ordinal.{v}) : Ordinal.lift.{u, v} (a * b) = Ordinal.lift.{u, v} a * Ordinal.lift.{u, v} b

@[simp]

theorem Ordinal.card_mul (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) : (a * b).card = a.card * b.card

instance Ordinal.leftDistribClass : LeftDistribClass Ordinal.{u}

Equations

• Ordinal.leftDistribClass = ⋯

theorem Ordinal.mul_succ (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) : a * Order.succ b = a * b + a

instance Ordinal.mulLeftMono : MulLeftMono Ordinal.{u}

Equations

• Ordinal.mulLeftMono = ⋯

instance Ordinal.mulRightMono : MulRightMono Ordinal.{u}

Equations

• Ordinal.mulRightMono = ⋯

theorem Ordinal.le_mul_left (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (hb : 0 < b) : a ≤ a * b

theorem Ordinal.le_mul_right (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (hb : 0 < b) : a ≤ b * a

theorem Ordinal.mul_le_of_limit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : b.IsLimit) : a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c

theorem Ordinal.isNormal_mul_right {a : Ordinal.{u_4}} (h : 0 < a) : Ordinal.IsNormal fun (x : Ordinal.{u_4}) => a * x

@[deprecated Ordinal.isNormal_mul_right]

theorem Ordinal.mul_isNormal {a : Ordinal.{u_4}} (h : 0 < a) : Ordinal.IsNormal fun (x : Ordinal.{u_4}) => a * x

Alias of Ordinal.isNormal_mul_right.

theorem Ordinal.lt_mul_of_limit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c.IsLimit) : a < b * c ↔ ∃ c' < c, a < b * c'

theorem Ordinal.mul_lt_mul_iff_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (a0 : 0 < a) : a * b < a * c ↔ b < c

theorem Ordinal.mul_le_mul_iff_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (a0 : 0 < a) : a * b ≤ a * c ↔ b ≤ c

theorem Ordinal.mul_lt_mul_of_pos_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : a < b) (c0 : 0 < c) : c * a < c * b

theorem Ordinal.mul_pos {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b

theorem Ordinal.mul_ne_zero {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} : a ≠ 0 → b ≠ 0 → a * b ≠ 0

theorem Ordinal.le_of_mul_le_mul_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c * a ≤ c * b) (h0 : 0 < c) : a ≤ b

theorem Ordinal.mul_right_inj {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (a0 : 0 < a) : a * b = a * c ↔ b = c

theorem Ordinal.isLimit_mul {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (a0 : 0 < a) : b.IsLimit → (a * b).IsLimit

@[deprecated Ordinal.isLimit_mul]

theorem Ordinal.mul_isLimit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (a0 : 0 < a) : b.IsLimit → (a * b).IsLimit

Alias of Ordinal.isLimit_mul.

theorem Ordinal.isLimit_mul_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (l : a.IsLimit) (b0 : 0 < b) : (a * b).IsLimit

@[deprecated Ordinal.isLimit_mul_left]

theorem Ordinal.mul_isLimit_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (l : a.IsLimit) (b0 : 0 < b) : (a * b).IsLimit

Alias of Ordinal.isLimit_mul_left.

theorem Ordinal.smul_eq_mul (n : ℕ) (a : Ordinal.{u_4}) : n • a = a * ↑n

Division on ordinals

instance Ordinal.div : Div Ordinal.{u_4}

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

Equations

• Ordinal.div = { div := fun (a b : Ordinal.{?u.6}) => if b = 0 then 0 else sInf {o : Ordinal.{?u.6} | a < b * Order.succ o} }

@[simp]

theorem Ordinal.div_zero (a : Ordinal.{u_4}) : a / 0 = 0

theorem Ordinal.lt_mul_succ_div (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b ≠ 0) : a < b * Order.succ (a / b)

theorem Ordinal.lt_mul_div_add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b ≠ 0) : a < b * (a / b) + b

theorem Ordinal.div_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (b0 : b ≠ 0) : a / b ≤ c ↔ a < b * Order.succ c

theorem Ordinal.lt_div {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c ≠ 0) : a < b / c ↔ c * Order.succ a ≤ b

theorem Ordinal.div_pos {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c ≠ 0) : 0 < b / c ↔ c ≤ b

theorem Ordinal.le_div {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (c0 : c ≠ 0) : a ≤ b / c ↔ c * a ≤ b

theorem Ordinal.div_lt {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (b0 : b ≠ 0) : a / b < c ↔ a < b * c

theorem Ordinal.div_le_of_le_mul {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : a ≤ b * c) : a / b ≤ c

theorem Ordinal.mul_lt_of_lt_div {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} : a < b / c → c * a < b

@[simp]

theorem Ordinal.zero_div (a : Ordinal.{u_4}) : 0 / a = 0

theorem Ordinal.mul_div_le (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) : b * (a / b) ≤ a

theorem Ordinal.div_le_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : a ≤ b) (c : Ordinal.{u_4}) : a / c ≤ b / c

theorem Ordinal.mul_add_div (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (b0 : b ≠ 0) (c : Ordinal.{u_4}) : (b * a + c) / b = a + c / b

theorem Ordinal.div_eq_zero_of_lt {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : a < b) : a / b = 0

@[simp]

theorem Ordinal.mul_div_cancel (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (b0 : b ≠ 0) : b * a / b = a

theorem Ordinal.mul_add_div_mul {a : Ordinal.{u_4}} {c : Ordinal.{u_4}} (hc : c < a) (b : Ordinal.{u_4}) (d : Ordinal.{u_4}) : (a * b + c) / (a * d) = b / d

theorem Ordinal.mul_div_mul_cancel {a : Ordinal.{u_4}} (ha : a ≠ 0) (b : Ordinal.{u_4}) (c : Ordinal.{u_4}) : a * b / (a * c) = b / c

@[simp]

theorem Ordinal.div_one (a : Ordinal.{u_4}) : a / 1 = a

@[simp]

theorem Ordinal.div_self {a : Ordinal.{u_4}} (h : a ≠ 0) : a / a = 1

theorem Ordinal.mul_sub (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) (c : Ordinal.{u_4}) : a * (b - c) = a * b - a * c

theorem Ordinal.isLimit_add_iff {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} : (a + b).IsLimit ↔ b.IsLimit ∨ b = 0 ∧ a.IsLimit

theorem Ordinal.dvd_add_iff {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} : a ∣ b → (a ∣ b + c ↔ a ∣ c)

theorem Ordinal.div_mul_cancel {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} : a ≠ 0 → a ∣ b → a * (b / a) = b

theorem Ordinal.le_of_dvd {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} : b ≠ 0 → a ∣ b → a ≤ b

theorem Ordinal.dvd_antisymm {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h₁ : a ∣ b) (h₂ : b ∣ a) : a = b

instance Ordinal.isAntisymm : IsAntisymm Ordinal.{u_4} fun (x1 x2 : Ordinal.{u_4}) => x1 ∣ x2

Equations

• Ordinal.isAntisymm = ⋯

instance Ordinal.mod : Mod Ordinal.{u_4}

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

Equations

• Ordinal.mod = { mod := fun (a b : Ordinal.{?u.5}) => a - b * (a / b) }

theorem Ordinal.mod_def (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) : a % b = a - b * (a / b)

theorem Ordinal.mod_le (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) : a % b ≤ a

@[simp]

theorem Ordinal.mod_zero (a : Ordinal.{u_4}) : a % 0 = a

theorem Ordinal.mod_eq_of_lt {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : a < b) : a % b = a

@[simp]

theorem Ordinal.zero_mod (b : Ordinal.{u_4}) : 0 % b = 0

theorem Ordinal.div_add_mod (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) : b * (a / b) + a % b = a

theorem Ordinal.mod_lt (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b ≠ 0) : a % b < b

@[simp]

theorem Ordinal.mod_self (a : Ordinal.{u_4}) : a % a = 0

@[simp]

theorem Ordinal.mod_one (a : Ordinal.{u_4}) : a % 1 = 0

theorem Ordinal.dvd_of_mod_eq_zero {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (H : a % b = 0) : b ∣ a

theorem Ordinal.mod_eq_zero_of_dvd {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (H : b ∣ a) : a % b = 0

theorem Ordinal.dvd_iff_mod_eq_zero {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} : b ∣ a ↔ a % b = 0

@[simp]

theorem Ordinal.mul_add_mod_self (x : Ordinal.{u_4}) (y : Ordinal.{u_4}) (z : Ordinal.{u_4}) : (x * y + z) % x = z % x

@[simp]

theorem Ordinal.mul_mod (x : Ordinal.{u_4}) (y : Ordinal.{u_4}) : x * y % x = 0

theorem Ordinal.mul_add_mod_mul {w : Ordinal.{u_4}} {x : Ordinal.{u_4}} (hw : w < x) (y : Ordinal.{u_4}) (z : Ordinal.{u_4}) : (x * y + w) % (x * z) = x * (y % z) + w

theorem Ordinal.mul_mod_mul (x : Ordinal.{u_4}) (y : Ordinal.{u_4}) (z : Ordinal.{u_4}) : x * y % (x * z) = x * (y % z)

theorem Ordinal.mod_mod_of_dvd (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c ∣ b) : a % b % c = a % c

@[simp]

theorem Ordinal.mod_mod (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) : a % b % b = a % b

Families of ordinals

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

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

def Ordinal.bfamilyOfFamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (a : Ordinal.{u}) : 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.bfamilyOfFamily' r f a ha = f ((Ordinal.enum r) ⟨a, ha⟩)

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

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

Equations

• Ordinal.bfamilyOfFamily = Ordinal.bfamilyOfFamily' WellOrderingRel

def Ordinal.familyOfBFamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → α) : ι → α

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

Equations

• Ordinal.familyOfBFamily' r ho f i = f ((Ordinal.typein r).toRelEmbedding i) ⋯

def Ordinal.familyOfBFamily {α : Type u_1} (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < o → α) : o.toType → α

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.familyOfBFamily f = Ordinal.familyOfBFamily' (fun (x1 x2 : o.toType) => x1 < x2) ⋯ f

@[simp]

theorem Ordinal.bfamilyOfFamily'_typein {α : Type u_1} {ι : Type u_4} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (i : ι) : Ordinal.bfamilyOfFamily' r f ((Ordinal.typein r).toRelEmbedding i) ⋯ = f i

@[simp]

theorem Ordinal.bfamilyOfFamily_typein {α : Type u_1} {ι : Type u_4} (f : ι → α) (i : ι) : Ordinal.bfamilyOfFamily f ((Ordinal.typein WellOrderingRel).toRelEmbedding i) ⋯ = f i

@[simp]

theorem Ordinal.familyOfBFamily'_enum {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → α) (i : Ordinal.{u}) (hi : i < o) : Ordinal.familyOfBFamily' r ho f ((Ordinal.enum r) ⟨i, ⋯⟩) = f i hi

@[simp]

theorem Ordinal.familyOfBFamily_enum {α : Type u_1} (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < o → α) (i : Ordinal.{u_4}) (hi : i < o) : o.familyOfBFamily f ((Ordinal.enum fun (x1 x2 : o.toType) => x1 < x2) ⟨i, ⋯⟩) = f i hi

def Ordinal.brange {α : Type u_1} (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < o → α) : Set α

The range of a family indexed by ordinals.

Equations

• o.brange f = {a : α | ∃ (i : Ordinal.{?u.30}) (hi : i < o), f i hi = a}

theorem Ordinal.mem_brange {α : Type u_1} {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → α} {a : α} : a ∈ o.brange f ↔ ∃ (i : Ordinal.{u_4}) (hi : i < o), f i hi = a

theorem Ordinal.mem_brange_self {α : Type u_1} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → α) (i : Ordinal.{u_4}) (hi : i < o) : f i hi ∈ o.brange f

@[simp]

theorem Ordinal.range_familyOfBFamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → α) : Set.range (Ordinal.familyOfBFamily' r ho f) = o.brange f

@[simp]

theorem Ordinal.range_familyOfBFamily {α : Type u_1} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → α) : Set.range (o.familyOfBFamily f) = o.brange f

@[simp]

theorem Ordinal.brange_bfamilyOfFamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) : (Ordinal.type r).brange (Ordinal.bfamilyOfFamily' r f) = Set.range f

@[simp]

theorem Ordinal.brange_bfamilyOfFamily {α : Type u_1} {ι : Type u} (f : ι → α) : (Ordinal.type WellOrderingRel).brange (Ordinal.bfamilyOfFamily f) = Set.range f

@[simp]

theorem Ordinal.brange_const {α : Type u_1} {o : Ordinal.{u_4}} (ho : o ≠ 0) {c : α} : (o.brange fun (x : Ordinal.{u_4}) (x : x < o) => c) = {c}

theorem Ordinal.comp_bfamilyOfFamily' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (g : α → β) : (fun (i : Ordinal.{u}) (hi : i < Ordinal.type r) => g (Ordinal.bfamilyOfFamily' r f i hi)) = Ordinal.bfamilyOfFamily' r (g ∘ f)

theorem Ordinal.comp_bfamilyOfFamily {α : Type u_1} {β : Type u_2} {ι : Type u} (f : ι → α) (g : α → β) : (fun (i : Ordinal.{u}) (hi : i < Ordinal.type WellOrderingRel) => g (Ordinal.bfamilyOfFamily f i hi)) = Ordinal.bfamilyOfFamily (g ∘ f)

theorem Ordinal.comp_familyOfBFamily' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → α) (g : α → β) : g ∘ Ordinal.familyOfBFamily' r ho f = Ordinal.familyOfBFamily' r ho fun (i : Ordinal.{u}) (hi : i < o) => g (f i hi)

theorem Ordinal.comp_familyOfBFamily {α : Type u_1} {β : Type u_2} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → α) (g : α → β) : g ∘ o.familyOfBFamily f = o.familyOfBFamily fun (i : Ordinal.{u_4}) (hi : i < o) => g (f i hi)

Supremum of a family of ordinals

@[deprecated iSup]

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

The supremum of a family of ordinals

Equations

• Ordinal.sup f = iSup f

@[deprecated]

theorem Ordinal.sSup_eq_sup {ι : Type u} (f : ι → Ordinal.{max u v} ) : sSup (Set.range f) = Ordinal.sup f

theorem Ordinal.bddAbove_range {ι : Type u} (f : ι → Ordinal.{max u v} ) : BddAbove (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.bddAbove_of_small (s : Set Ordinal.{u}) [h : Small.{u, u + 1} ↑s] : BddAbove s

theorem Ordinal.bddAbove_iff_small {s : Set Ordinal.{u}} : BddAbove s ↔ Small.{u, u + 1} ↑s

theorem Ordinal.bddAbove_image {s : Set Ordinal.{u}} (hf : BddAbove s) (f : Ordinal.{u} → Ordinal.{max u v} ) : BddAbove (f '' s)

theorem Ordinal.bddAbove_range_comp {ι : Type u} {f : ι → Ordinal.{v}} (hf : BddAbove (Set.range f)) (g : Ordinal.{v} → Ordinal.{max v w} ) : BddAbove (Set.range (g ∘ f))

theorem Ordinal.le_iSup {ι : Type u_4} (f : ι → Ordinal.{u}) [Small.{u, u_4} ι] (i : ι) : f i ≤ iSup f

le_ciSup whenever the input type is small in the output universe. This lemma sometimes fails to infer f in simple cases and needs it to be given explicitly.

@[deprecated Ordinal.le_iSup]

theorem Ordinal.le_sup {ι : Type u} (f : ι → Ordinal.{max u v} ) (i : ι) : f i ≤ Ordinal.sup f

theorem Ordinal.iSup_le_iff {ι : Type u_4} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_4} ι] : iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a

ciSup_le_iff' whenever the input type is small in the output universe.

@[deprecated Ordinal.iSup_le_iff]

theorem Ordinal.sup_le_iff {ι : Type u} {f : ι → Ordinal.{max u v} } {a : Ordinal.{max u v} } : Ordinal.sup f ≤ a ↔ ∀ (i : ι), f i ≤ a

theorem Ordinal.iSup_le {ι : Sort u_4} {f : ι → Ordinal.{u_5}} {a : Ordinal.{u_5}} : (∀ (i : ι), f i ≤ a) → iSup f ≤ a

An alias of ciSup_le' for discoverability.

@[deprecated Ordinal.iSup_le]

theorem Ordinal.sup_le {ι : Type u} {f : ι → Ordinal.{max u v} } {a : Ordinal.{max u v} } : (∀ (i : ι), f i ≤ a) → Ordinal.sup f ≤ a

theorem Ordinal.lt_iSup {ι : Type u_4} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_4} ι] : a < iSup f ↔ ∃ (i : ι), a < f i

lt_ciSup_iff' whenever the input type is small in the output universe.

@[deprecated Ordinal.lt_iSup]

theorem Ordinal.lt_sup {ι : Type u} {f : ι → Ordinal.{max u v} } {a : Ordinal.{max u v} } : a < Ordinal.sup f ↔ ∃ (i : ι), a < f i

@[deprecated]

theorem Ordinal.ne_iSup_iff_lt_iSup {ι : Type u} {f : ι → Ordinal.{max u v} } : (∀ (i : ι), f i ≠ iSup f) ↔ ∀ (i : ι), f i < iSup f

@[deprecated Ordinal.ne_iSup_iff_lt_iSup]

theorem Ordinal.ne_sup_iff_lt_sup {ι : Type u} {f : ι → Ordinal.{max u v} } : (∀ (i : ι), f i ≠ Ordinal.sup f) ↔ ∀ (i : ι), f i < Ordinal.sup f

theorem Ordinal.succ_lt_iSup_of_ne_iSup {ι : Type u_4} {f : ι → Ordinal.{u}} [Small.{u, u_4} ι] (hf : ∀ (i : ι), f i ≠ iSup f) {a : Ordinal.{u}} (hao : a < iSup f) : Order.succ a < iSup f

@[deprecated Ordinal.succ_lt_iSup_of_ne_iSup]

theorem Ordinal.sup_not_succ_of_ne_sup {ι : Type u} {f : ι → Ordinal.{max u v} } (hf : ∀ (i : ι), f i ≠ Ordinal.sup f) {a : Ordinal.{max u v} } (hao : a < Ordinal.sup f) : Order.succ a < Ordinal.sup f

theorem Ordinal.iSup_eq_zero_iff {ι : Type u_4} {f : ι → Ordinal.{u}} [Small.{u, u_4} ι] : iSup f = 0 ↔ ∀ (i : ι), f i = 0

@[deprecated Ordinal.iSup_eq_zero_iff]

theorem Ordinal.sup_eq_zero_iff {ι : Type u} {f : ι → Ordinal.{max u v} } : Ordinal.sup f = 0 ↔ ∀ (i : ι), f i = 0

@[deprecated ciSup_of_empty]

theorem Ordinal.sup_empty {ι : Type u_4} [IsEmpty ι] (f : ι → Ordinal.{max u_5 u_4} ) : Ordinal.sup f = 0

@[deprecated ciSup_const]

theorem Ordinal.sup_const {ι : Type u_4} [_hι : Nonempty ι] (o : Ordinal.{max u_5 u_4} ) : (Ordinal.sup fun (x : ι) => o) = o

@[deprecated ciSup_unique]

theorem Ordinal.sup_unique {ι : Type u_4} [Unique ι] (f : ι → Ordinal.{max u_5 u_4} ) : Ordinal.sup f = f default

@[deprecated csSup_le_csSup']

theorem Ordinal.sup_le_of_range_subset {ι : Type u} {ι' : Type v} {f : ι → Ordinal.{max (max u v) w} } {g : ι' → Ordinal.{max (max u v) w} } (h : Set.range f ⊆ Set.range g) : Ordinal.sup f ≤ Ordinal.sup g

theorem Ordinal.iSup_eq_of_range_eq {ι : Sort u_4} {ι' : Sort u_5} {f : ι → Ordinal.{u_6}} {g : ι' → Ordinal.{u_6}} (h : Set.range f = Set.range g) : iSup f = iSup g

@[deprecated Ordinal.iSup_eq_of_range_eq]

theorem Ordinal.sup_eq_of_range_eq {ι : Type u} {ι' : Type v} {f : ι → Ordinal.{max u v w} } {g : ι' → Ordinal.{max u v w} } (h : Set.range f = Set.range g) : Ordinal.sup f = Ordinal.sup g

theorem Ordinal.iSup_sum {α : Type u_4} {β : Type u_5} (f : α ⊕ β → Ordinal.{u}) [Small.{u, u_4} α] [Small.{u, u_5} β] : iSup f = max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))

@[deprecated Ordinal.iSup_sum]

theorem Ordinal.sup_sum {α : Type u} {β : Type v} (f : α ⊕ β → Ordinal.{max (max u v) w} ) : Ordinal.sup f = max (Ordinal.sup fun (a : α) => f (Sum.inl a)) (Ordinal.sup fun (b : β) => f (Sum.inr b))

theorem Ordinal.unbounded_range_of_le_iSup {α : Type u} {β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β → α) (h : Ordinal.type r ≤ ⨆ (i : β), (Ordinal.typein r).toRelEmbedding (f i)) : Set.Unbounded r (Set.range f)

@[deprecated Ordinal.unbounded_range_of_le_iSup]

theorem Ordinal.unbounded_range_of_sup_ge {α : Type u} {β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β → α) (h : Ordinal.type r ≤ Ordinal.sup (⇑(Ordinal.typein r).toRelEmbedding ∘ f)) : Set.Unbounded r (Set.range f)

@[deprecated]

theorem Ordinal.le_sup_shrink_equiv {s : Set Ordinal.{u}} (hs : Small.{u, u + 1} ↑s) (a : Ordinal.{u}) (ha : a ∈ s) : a ≤ Ordinal.sup fun (x : Shrink.{u, u + 1} ↑s) => ↑((equivShrink ↑s).symm x)

theorem Ordinal.IsNormal.map_iSup_of_bddAbove {f : Ordinal.{u} → Ordinal.{v}} (H : Ordinal.IsNormal f) {ι : Type u_4} (g : ι → Ordinal.{u}) (hg : BddAbove (Set.range g)) [Nonempty ι] : f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

theorem Ordinal.IsNormal.map_iSup {f : Ordinal.{u} → Ordinal.{v}} (H : Ordinal.IsNormal f) {ι : Type w} (g : ι → Ordinal.{u}) [Small.{u, w} ι] [Nonempty ι] : f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

theorem Ordinal.IsNormal.map_sSup_of_bddAbove {f : Ordinal.{u} → Ordinal.{v}} (H : Ordinal.IsNormal f) {s : Set Ordinal.{u}} (hs : BddAbove s) (hn : s.Nonempty) : f (sSup s) = sSup (f '' s)

theorem Ordinal.IsNormal.map_sSup {f : Ordinal.{u} → Ordinal.{v}} (H : Ordinal.IsNormal f) {s : Set Ordinal.{u}} (hn : s.Nonempty) [Small.{u, u + 1} ↑s] : f (sSup s) = sSup (f '' s)

@[deprecated Ordinal.IsNormal.map_iSup]

theorem Ordinal.IsNormal.sup {f : Ordinal.{max u v} → Ordinal.{max u w} } (H : Ordinal.IsNormal f) {ι : Type u} (g : ι → Ordinal.{max u v} ) [Nonempty ι] : f (Ordinal.sup g) = Ordinal.sup (f ∘ g)

theorem Ordinal.IsNormal.apply_of_isLimit {f : Ordinal.{u} → Ordinal.{v}} (H : Ordinal.IsNormal f) {o : Ordinal.{u}} (ho : o.IsLimit) : f o = ⨆ (a : ↑(Set.Iio o)), f ↑a

@[deprecated]

theorem Ordinal.sup_eq_sSup {s : Set Ordinal.{u}} (hs : Small.{u, u + 1} ↑s) : (Ordinal.sup fun (x : Shrink.{u, u + 1} ↑s) => ↑((equivShrink ↑s).symm x)) = sSup s

theorem Ordinal.sSup_ord {s : Set Cardinal.{u}} (hs : BddAbove s) : (sSup s).ord = sSup (Cardinal.ord '' s)

theorem Ordinal.iSup_ord {ι : Sort u_4} {f : ι → Cardinal.{u_5}} (hf : BddAbove (Set.range f)) : (iSup f).ord = ⨆ (i : ι), (f i).ord

theorem Ordinal.sInf_compl_lt_lift_ord_succ {ι : Type u} (f : ι → Ordinal.{max u v} ) : sInf (Set.range f)ᶜ < Ordinal.lift.{v, u} (Order.succ (Cardinal.mk ι)).ord

theorem Ordinal.sInf_compl_lt_ord_succ {ι : Type u} (f : ι → Ordinal.{u}) : sInf (Set.range f)ᶜ < (Order.succ (Cardinal.mk ι)).ord

theorem Ordinal.sup_eq_sup {ι : Type u} {ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (ho' : Ordinal.type r' = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : Ordinal.sup (Ordinal.familyOfBFamily' r ho f) = Ordinal.sup (Ordinal.familyOfBFamily' r' ho' f)

def Ordinal.bsup (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : Ordinal.{max u v}

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

Equations

• o.bsup f = Ordinal.sup (o.familyOfBFamily f)

@[simp]

theorem Ordinal.sup_eq_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : Ordinal.sup (o.familyOfBFamily f) = o.bsup f

@[simp]

theorem Ordinal.sup_eq_bsup' {o : Ordinal.{u}} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : Ordinal.sup (Ordinal.familyOfBFamily' r ho f) = o.bsup f

@[simp]

theorem Ordinal.sSup_eq_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : sSup (o.brange f) = o.bsup f

@[simp]

theorem Ordinal.bsup_eq_sup' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u v} ) : (Ordinal.type r).bsup (Ordinal.bfamilyOfFamily' r f) = Ordinal.sup f

theorem Ordinal.bsup_eq_bsup {ι : Type u} (r : ι → ι → Prop) (r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r'] (f : ι → Ordinal.{max u v} ) : (Ordinal.type r).bsup (Ordinal.bfamilyOfFamily' r f) = (Ordinal.type r').bsup (Ordinal.bfamilyOfFamily' r' f)

@[simp]

theorem Ordinal.bsup_eq_sup {ι : Type u} (f : ι → Ordinal.{max u v} ) : (Ordinal.type WellOrderingRel).bsup (Ordinal.bfamilyOfFamily f) = Ordinal.sup f

theorem Ordinal.bsup_congr {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v} ) (ho : o₁ = o₂) : o₁.bsup f = o₂.bsup fun (a : Ordinal.{u}) (h : a < o₂) => f a ⋯

theorem Ordinal.bsup_le_iff {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} } {a : Ordinal.{max u v} } : o.bsup f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h ≤ a

theorem Ordinal.bsup_le {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} } {a : Ordinal.{max u v} } : (∀ (i : Ordinal.{u}) (h : i < o), f i h ≤ a) → o.bsup f ≤ a

theorem Ordinal.le_bsup {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4} ) (i : Ordinal.{u_4}) (h : i < o) : f i h ≤ o.bsup f

theorem Ordinal.lt_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) {a : Ordinal.{max u v} } : a < o.bsup f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), a < f i hi

theorem Ordinal.IsNormal.bsup {f : Ordinal.{max u v} → Ordinal.{max u w} } (H : Ordinal.IsNormal f) {o : Ordinal.{u}} (g : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : o ≠ 0 → f (o.bsup g) = o.bsup fun (a : Ordinal.{u}) (h : a < o) => f (g a h)

theorem Ordinal.lt_bsup_of_ne_bsup {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} } : (∀ (i : Ordinal.{u}) (h : i < o), f i h ≠ o.bsup f) ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f

theorem Ordinal.bsup_not_succ_of_ne_bsup {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} } (hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ o.bsup f) (a : Ordinal.{max u v} ) : a < o.bsup f → Order.succ a < o.bsup f

@[simp]

theorem Ordinal.bsup_eq_zero_iff {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4} } : o.bsup f = 0 ↔ ∀ (i : Ordinal.{u_4}) (hi : i < o), f i hi = 0

theorem Ordinal.lt_bsup_of_limit {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5} } (hf : ∀ {a a' : Ordinal.{u_4}} (ha : a < o) (ha' : a' < o), a < a' → f a ha < f a' ha') (ho : ∀ a < o, Order.succ a < o) (i : Ordinal.{u_4}) (h : i < o) : f i h < o.bsup f

theorem Ordinal.bsup_succ_of_mono {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < Order.succ o → Ordinal.{max u_4 u_5} } (hf : ∀ {i j : Ordinal.{u_4}} (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.{u_4}) → a < 0 → Ordinal.{max u_4 u_5} ) : Ordinal.bsup 0 f = 0

theorem Ordinal.bsup_const {o : Ordinal.{u}} (ho : o ≠ 0) (a : Ordinal.{max u v} ) : (o.bsup fun (x : Ordinal.{u}) (x : x < o) => a) = a

@[simp]

theorem Ordinal.bsup_one (f : (a : Ordinal.{u_4}) → a < 1 → Ordinal.{max u_4 u_5} ) : Ordinal.bsup 1 f = f 0 ⋯

theorem Ordinal.bsup_le_of_brange_subset {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w} } {g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w} } (h : o.brange f ⊆ o'.brange g) : o.bsup f ≤ o'.bsup g

theorem Ordinal.bsup_eq_of_brange_eq {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w} } {g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w} } (h : o.brange f = o'.brange g) : o.bsup f = o'.bsup g

def Ordinal.lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4} ) : Ordinal.{max u_5 u_4}

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} (f : ι → Ordinal.{max u v} ) : Ordinal.sup (Order.succ ∘ f) = Ordinal.lsub f

theorem Ordinal.lsub_le_iff {ι : Type u} {f : ι → Ordinal.{max u v} } {a : Ordinal.{max v u} } : Ordinal.lsub f ≤ a ↔ ∀ (i : ι), f i < a

theorem Ordinal.lsub_le {ι : Type u_4} {f : ι → Ordinal.{max u_5 u_4} } {a : Ordinal.{max u_5 u_4} } : (∀ (i : ι), f i < a) → Ordinal.lsub f ≤ a

theorem Ordinal.lt_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4} ) (i : ι) : f i < Ordinal.lsub f

theorem Ordinal.lt_lsub_iff {ι : Type u} {f : ι → Ordinal.{max u v} } {a : Ordinal.{max v u} } : a < Ordinal.lsub f ↔ ∃ (i : ι), a ≤ f i

theorem Ordinal.sup_le_lsub {ι : Type u} (f : ι → Ordinal.{max u v} ) : Ordinal.sup f ≤ Ordinal.lsub f

theorem Ordinal.lsub_le_sup_succ {ι : Type u} (f : ι → Ordinal.{max u v} ) : Ordinal.lsub f ≤ Order.succ (Ordinal.sup f)

theorem Ordinal.sup_eq_lsub_or_sup_succ_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v} ) : Ordinal.sup f = Ordinal.lsub f ∨ Order.succ (Ordinal.sup f) = Ordinal.lsub f

theorem Ordinal.sup_succ_le_lsub {ι : Type u} (f : ι → Ordinal.{max u v} ) : Order.succ (Ordinal.sup f) ≤ Ordinal.lsub f ↔ ∃ (i : ι), f i = Ordinal.sup f

theorem Ordinal.sup_succ_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v} ) : Order.succ (Ordinal.sup f) = Ordinal.lsub f ↔ ∃ (i : ι), f i = Ordinal.sup f

theorem Ordinal.sup_eq_lsub_iff_succ {ι : Type u} (f : ι → Ordinal.{max u v} ) : Ordinal.sup f = Ordinal.lsub f ↔ ∀ a < Ordinal.lsub f, Order.succ a < Ordinal.lsub f

theorem Ordinal.sup_eq_lsub_iff_lt_sup {ι : Type u} (f : ι → Ordinal.{max u v} ) : Ordinal.sup f = Ordinal.lsub f ↔ ∀ (i : ι), f i < Ordinal.sup f

@[simp]

theorem Ordinal.lsub_empty {ι : Type u_4} [h : IsEmpty ι] (f : ι → Ordinal.{max u_5 u_4} ) : Ordinal.lsub f = 0

theorem Ordinal.lsub_pos {ι : Type u} [h : Nonempty ι] (f : ι → Ordinal.{max u v} ) : 0 < Ordinal.lsub f

@[simp]

theorem Ordinal.lsub_eq_zero_iff {ι : Type u} (f : ι → Ordinal.{max u v} ) : Ordinal.lsub f = 0 ↔ IsEmpty ι

@[simp]

theorem Ordinal.lsub_const {ι : Type u_4} [Nonempty ι] (o : Ordinal.{max u_5 u_4} ) : (Ordinal.lsub fun (x : ι) => o) = Order.succ o

@[simp]

theorem Ordinal.lsub_unique {ι : Type u_4} [Unique ι] (f : ι → Ordinal.{max u_5 u_4} ) : Ordinal.lsub f = Order.succ (f default)

theorem Ordinal.lsub_le_of_range_subset {ι : Type u} {ι' : Type v} {f : ι → Ordinal.{max (max u v) w} } {g : ι' → Ordinal.{max (max u v) w} } (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.{max (max u v) w} } {g : ι' → Ordinal.{max (max u v) w} } (h : Set.range f = Set.range g) : Ordinal.lsub f = Ordinal.lsub g

@[simp]

theorem Ordinal.lsub_sum {α : Type u} {β : Type v} (f : α ⊕ β → Ordinal.{max (max u v) w} ) : Ordinal.lsub f = max (Ordinal.lsub fun (a : α) => f (Sum.inl a)) (Ordinal.lsub fun (b : β) => f (Sum.inr b))

theorem Ordinal.lsub_not_mem_range {ι : Type u} (f : ι → Ordinal.{max u v} ) : Ordinal.lsub f ∉ Set.range f

theorem Ordinal.nonempty_compl_range {ι : Type u} (f : ι → Ordinal.{max u v} ) : (Set.range f)ᶜ.Nonempty

@[simp]

theorem Ordinal.lsub_typein (o : Ordinal.{u}) : Ordinal.lsub ⇑(Ordinal.typein fun (x1 x2 : o.toType) => x1 < x2).toRelEmbedding = o

theorem Ordinal.sup_typein_limit {o : Ordinal.{u}} (ho : ∀ a < o, Order.succ a < o) : Ordinal.sup ⇑(Ordinal.typein fun (x1 x2 : o.toType) => x1 < x2).toRelEmbedding = o

@[simp]

theorem Ordinal.sup_typein_succ {o : Ordinal.{u}} : Ordinal.sup ⇑(Ordinal.typein fun (x1 x2 : (Order.succ o).toType) => x1 < x2).toRelEmbedding = o

def Ordinal.blsub (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : Ordinal.{max u v}

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

This is to lsub as bsup is to sup.

Equations

• o.blsub f = o.bsup fun (a : Ordinal.{?u.31}) (ha : a < o) => Order.succ (f a ha)

@[simp]

theorem Ordinal.bsup_eq_blsub (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : (o.bsup fun (a : Ordinal.{u}) (ha : a < o) => Order.succ (f a ha)) = o.blsub f

theorem Ordinal.lsub_eq_blsub' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : Ordinal.lsub (Ordinal.familyOfBFamily' r ho f) = o.blsub f

theorem Ordinal.lsub_eq_lsub {ι : Type u} {ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (ho' : Ordinal.type r' = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : Ordinal.lsub (Ordinal.familyOfBFamily' r ho f) = Ordinal.lsub (Ordinal.familyOfBFamily' r' ho' f)

@[simp]

theorem Ordinal.lsub_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : Ordinal.lsub (o.familyOfBFamily f) = o.blsub f

@[simp]

theorem Ordinal.blsub_eq_lsub' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u v} ) : (Ordinal.type r).blsub (Ordinal.bfamilyOfFamily' r f) = Ordinal.lsub f

theorem Ordinal.blsub_eq_blsub {ι : Type u} (r : ι → ι → Prop) (r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r'] (f : ι → Ordinal.{max u v} ) : (Ordinal.type r).blsub (Ordinal.bfamilyOfFamily' r f) = (Ordinal.type r').blsub (Ordinal.bfamilyOfFamily' r' f)

@[simp]

theorem Ordinal.blsub_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v} ) : (Ordinal.type WellOrderingRel).blsub (Ordinal.bfamilyOfFamily f) = Ordinal.lsub f

theorem Ordinal.blsub_congr {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v} ) (ho : o₁ = o₂) : o₁.blsub f = o₂.blsub fun (a : Ordinal.{u}) (h : a < o₂) => f a ⋯

theorem Ordinal.blsub_le_iff {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} } {a : Ordinal.{max u v} } : o.blsub f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < a

theorem Ordinal.blsub_le {o : Ordinal.{u_4}} {f : (b : Ordinal.{u_4}) → b < o → Ordinal.{max u_4 u_5} } {a : Ordinal.{max u_4 u_5} } : (∀ (i : Ordinal.{u_4}) (h : i < o), f i h < a) → o.blsub f ≤ a

theorem Ordinal.lt_blsub {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4} ) (i : Ordinal.{u_4}) (h : i < o) : f i h < o.blsub f

theorem Ordinal.lt_blsub_iff {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} } {a : Ordinal.{max u v} } : a < o.blsub f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), a ≤ f i hi

theorem Ordinal.bsup_le_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : o.bsup f ≤ o.blsub f

theorem Ordinal.blsub_le_bsup_succ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : o.blsub f ≤ Order.succ (o.bsup f)

theorem Ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : o.bsup f = o.blsub f ∨ Order.succ (o.bsup f) = o.blsub f

theorem Ordinal.bsup_succ_le_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : Order.succ (o.bsup f) ≤ o.blsub f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o.bsup f

theorem Ordinal.bsup_succ_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : Order.succ (o.bsup f) = o.blsub f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o.bsup f

theorem Ordinal.bsup_eq_blsub_iff_succ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : o.bsup f = o.blsub f ↔ ∀ a < o.blsub f, Order.succ a < o.blsub f

theorem Ordinal.bsup_eq_blsub_iff_lt_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : o.bsup f = o.blsub f ↔ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < o.bsup f

theorem Ordinal.bsup_eq_blsub_of_lt_succ_limit {o : Ordinal.{u}} (ho : o.IsLimit) {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} } (hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (Order.succ a) ⋯) : o.bsup f = o.blsub f

theorem Ordinal.blsub_succ_of_mono {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < Order.succ o → Ordinal.{max u v} } (hf : ∀ {i j : Ordinal.{u}} (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.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4} } : o.blsub f = 0 ↔ o = 0

@[simp]

theorem Ordinal.blsub_zero (f : (a : Ordinal.{u_4}) → a < 0 → Ordinal.{max u_4 u_5} ) : Ordinal.blsub 0 f = 0

theorem Ordinal.blsub_pos {o : Ordinal.{u_4}} (ho : 0 < o) (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5} ) : 0 < o.blsub f

theorem Ordinal.blsub_type {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : (a : Ordinal.{u}) → a < Ordinal.type r → Ordinal.{max u v} ) : (Ordinal.type r).blsub f = Ordinal.lsub fun (a : α) => f ((Ordinal.typein r).toRelEmbedding a) ⋯

theorem Ordinal.blsub_const {o : Ordinal.{u}} (ho : o ≠ 0) (a : Ordinal.{max u v} ) : (o.blsub fun (x : Ordinal.{u}) (x : x < o) => a) = Order.succ a

@[simp]

theorem Ordinal.blsub_one (f : (a : Ordinal.{u_4}) → a < 1 → Ordinal.{max u_4 u_5} ) : Ordinal.blsub 1 f = Order.succ (f 0 ⋯)

@[simp]

theorem Ordinal.blsub_id (o : Ordinal.{u}) : (o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => x) = o

theorem Ordinal.bsup_id_limit {o : Ordinal.{u}} : (∀ a < o, Order.succ a < o) → (o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => x) = o

@[simp]

theorem Ordinal.bsup_id_succ (o : Ordinal.{u}) : ((Order.succ o).bsup fun (x : Ordinal.{u}) (x_1 : x < Order.succ o) => x) = o

theorem Ordinal.blsub_le_of_brange_subset {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w} } {g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w} } (h : o.brange f ⊆ o'.brange g) : o.blsub f ≤ o'.blsub g

theorem Ordinal.blsub_eq_of_brange_eq {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w} } {g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w} } (h : {o_1 : Ordinal.{max (max u v) w} | ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o_1} = {o : Ordinal.{max (max u v) w} | ∃ (i : Ordinal.{v}) (hi : i < o'), g i hi = o}) : o.blsub f = o'.blsub g

theorem Ordinal.bsup_comp {o : Ordinal.{max u v} } {o' : Ordinal.{max u v} } {f : (a : Ordinal.{max u v} ) → a < o → Ordinal.{max u v w} } (hf : ∀ {i j : Ordinal.{max u v} } (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj) {g : (a : Ordinal.{max u v} ) → a < o' → Ordinal.{max u v} } (hg : o'.blsub g = o) : (o'.bsup fun (a : Ordinal.{max u v} ) (ha : a < o') => f (g a ha) ⋯) = o.bsup f

theorem Ordinal.blsub_comp {o : Ordinal.{max u v} } {o' : Ordinal.{max u v} } {f : (a : Ordinal.{max u v} ) → a < o → Ordinal.{max u v w} } (hf : ∀ {i j : Ordinal.{max u v} } (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj) {g : (a : Ordinal.{max u v} ) → a < o' → Ordinal.{max u v} } (hg : o'.blsub g = o) : (o'.blsub fun (a : Ordinal.{max u v} ) (ha : a < o') => f (g a ha) ⋯) = o.blsub f

theorem Ordinal.IsNormal.bsup_eq {f : Ordinal.{u} → Ordinal.{max u v} } (H : Ordinal.IsNormal f) {o : Ordinal.{u}} (h : o.IsLimit) : (o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o

theorem Ordinal.IsNormal.blsub_eq {f : Ordinal.{u} → Ordinal.{max u v} } (H : Ordinal.IsNormal f) {o : Ordinal.{u}} (h : o.IsLimit) : (o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o

theorem Ordinal.isNormal_iff_lt_succ_and_bsup_eq {f : Ordinal.{u} → Ordinal.{max u v} } : Ordinal.IsNormal f ↔ (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧ ∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o

theorem Ordinal.isNormal_iff_lt_succ_and_blsub_eq {f : Ordinal.{u} → Ordinal.{max u v} } : Ordinal.IsNormal f ↔ (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧ ∀ (o : Ordinal.{u}), o.IsLimit → (o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o

theorem Ordinal.IsNormal.eq_iff_zero_and_succ {f : Ordinal.{u} → Ordinal.{u}} {g : Ordinal.{u} → Ordinal.{u}} (hf : Ordinal.IsNormal f) (hg : Ordinal.IsNormal g) : f = g ↔ f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (Order.succ a) = g (Order.succ a)

@[deprecated]

def Ordinal.blsub₂ (o₁ : Ordinal.{u_4}) (o₂ : Ordinal.{u_5}) (op : {a : Ordinal.{u_4}} → a < o₁ → {b : Ordinal.{u_5}} → b < o₂ → Ordinal.{max (max u_6 u_4) u_5} ) : Ordinal.{max u_6 u_4 u_5}

A two-argument version of Ordinal.blsub.

Deprecated. If you need this value explicitly, write it in terms of iSup. If you just want an upper bound for the image of op, use that Iio a ×ˢ Iio b is a small set.

Equations

• o₁.blsub₂ o₂ op = Ordinal.lsub fun (x : o₁.toType × o₂.toType) => op ⋯ ⋯

@[deprecated]

theorem Ordinal.lt_blsub₂ {o₁ : Ordinal.{u_4}} {o₂ : Ordinal.{u_5}} (op : {a : Ordinal.{u_4}} → a < o₁ → {b : Ordinal.{u_5}} → b < o₂ → Ordinal.{max (max u_4 u_5) u_6} ) {a : Ordinal.{u_4}} {b : Ordinal.{u_5}} (ha : a < o₁) (hb : b < o₂) : op ha hb < o₁.blsub₂ o₂ fun {a : Ordinal.{u_4}} => op

Minimum excluded ordinals

@[deprecated]

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

The minimum excluded ordinal in a family of ordinals.

Equations

• Ordinal.mex f = sInf (Set.range f)ᶜ

@[deprecated]

theorem Ordinal.mex_not_mem_range {ι : Type u} (f : ι → Ordinal.{max u v} ) : Ordinal.mex f ∉ Set.range f

@[deprecated]

theorem Ordinal.le_mex_of_forall {ι : Type u} {f : ι → Ordinal.{max u v} } {a : Ordinal.{max u v} } (H : ∀ b < a, ∃ (i : ι), f i = b) : a ≤ Ordinal.mex f

@[deprecated]

theorem Ordinal.ne_mex {ι : Type u} (f : ι → Ordinal.{max u v} ) (i : ι) : f i ≠ Ordinal.mex f

@[deprecated]

theorem Ordinal.mex_le_of_ne {ι : Type u_4} {f : ι → Ordinal.{max u_5 u_4} } {a : Ordinal.{max u_5 u_4} } (ha : ∀ (i : ι), f i ≠ a) : Ordinal.mex f ≤ a

@[deprecated]

theorem Ordinal.exists_of_lt_mex {ι : Type u_4} {f : ι → Ordinal.{max u_5 u_4} } {a : Ordinal.{max u_4 u_5} } (ha : a < Ordinal.mex f) : ∃ (i : ι), f i = a

@[deprecated]

theorem Ordinal.mex_le_lsub {ι : Type u} (f : ι → Ordinal.{max u v} ) : Ordinal.mex f ≤ Ordinal.lsub f

@[deprecated]

theorem Ordinal.mex_monotone {α : Type u} {β : Type u} {f : α → Ordinal.{max u v} } {g : β → Ordinal.{max u v} } (h : Set.range f ⊆ Set.range g) : Ordinal.mex f ≤ Ordinal.mex g

@[deprecated Ordinal.sInf_compl_lt_ord_succ]

theorem Ordinal.mex_lt_ord_succ_mk {ι : Type u} (f : ι → Ordinal.{u}) : Ordinal.mex f < (Order.succ (Cardinal.mk ι)).ord

@[deprecated]

def Ordinal.bmex (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5} ) : Ordinal.{max u_5 u_4}

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

This is to mex as bsup is to sup.

Equations

• o.bmex f = Ordinal.mex (o.familyOfBFamily f)

@[deprecated]

theorem Ordinal.bmex_not_mem_brange {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5} ) : o.bmex f ∉ o.brange f

@[deprecated]

theorem Ordinal.le_bmex_of_forall {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5} ) {a : Ordinal.{max u_4 u_5} } (H : ∀ b < a, ∃ (i : Ordinal.{u_4}) (hi : i < o), f i hi = b) : a ≤ o.bmex f

@[deprecated]

theorem Ordinal.ne_bmex {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) {i : Ordinal.{u}} (hi : i < o) : f i hi ≠ o.bmex f

@[deprecated]

theorem Ordinal.bmex_le_of_ne {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5} } {a : Ordinal.{max u_4 u_5} } (ha : ∀ (i : Ordinal.{u_4}) (hi : i < o), f i hi ≠ a) : o.bmex f ≤ a

@[deprecated]

theorem Ordinal.exists_of_lt_bmex {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5} } {a : Ordinal.{max u_5 u_4} } (ha : a < o.bmex f) : ∃ (i : Ordinal.{u_4}) (hi : i < o), f i hi = a

@[deprecated]

theorem Ordinal.bmex_le_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : o.bmex f ≤ o.blsub f

@[deprecated]

theorem Ordinal.bmex_monotone {o : Ordinal.{u}} {o' : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} } {g : (a : Ordinal.{u}) → a < o' → Ordinal.{max u v} } (h : o.brange f ⊆ o'.brange g) : o.bmex f ≤ o'.bmex g

@[deprecated Ordinal.sInf_compl_lt_ord_succ]

theorem Ordinal.bmex_lt_ord_succ_card {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}) : o.bmex f < (Order.succ o.card).ord

Results about injectivity and surjectivity

theorem not_surjective_of_ordinal {α : Type u} (f : α → Ordinal.{u}) : ¬Function.Surjective f

theorem not_injective_of_ordinal {α : Type u} (f : Ordinal.{u} → α) : ¬Function.Injective f

theorem not_surjective_of_ordinal_of_small {α : Type v} [Small.{u, v} α] (f : α → Ordinal.{u}) : ¬Function.Surjective f

theorem not_injective_of_ordinal_of_small {α : Type v} [Small.{u, v} α] (f : Ordinal.{u} → α) : ¬Function.Injective f

theorem not_small_ordinal : ¬Small.{u, max (u + 1) (v + 1)} Ordinal.{max u v}

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

theorem Ordinal.not_bddAbove_compl_of_small (s : Set Ordinal.{u}) [hs : Small.{u, u + 1} ↑s] : ¬BddAbove sᶜ

Casting naturals into ordinals, compatibility with operations

instance Ordinal.instCharZero : CharZero Ordinal.{u_1}

Equations

• Ordinal.instCharZero = ⋯

@[simp]

theorem Ordinal.one_add_natCast (m : ℕ) : 1 + ↑m = ↑(Order.succ m)

@[deprecated Ordinal.one_add_natCast]

theorem Ordinal.one_add_nat_cast (m : ℕ) : 1 + ↑m = ↑(Order.succ m)

Alias of Ordinal.one_add_natCast.

@[simp]

theorem Ordinal.one_add_ofNat (m : ℕ) [m.AtLeastTwo] : 1 + OfNat.ofNat m = Order.succ (OfNat.ofNat m)

@[simp]

theorem Ordinal.natCast_mul (m : ℕ) (n : ℕ) : ↑(m * n) = ↑m * ↑n

@[deprecated Ordinal.natCast_mul]

theorem Ordinal.nat_cast_mul (m : ℕ) (n : ℕ) : ↑(m * n) = ↑m * ↑n

Alias of Ordinal.natCast_mul.

@[deprecated Nat.cast_le]

theorem Ordinal.natCast_le {m : ℕ} {n : ℕ} : ↑m ≤ ↑n ↔ m ≤ n

@[deprecated Ordinal.natCast_le]

theorem Ordinal.nat_cast_le {m : ℕ} {n : ℕ} : ↑m ≤ ↑n ↔ m ≤ n

Alias of Ordinal.natCast_le.

@[deprecated Nat.cast_inj]

theorem Ordinal.natCast_inj {m : ℕ} {n : ℕ} : ↑m = ↑n ↔ m = n

@[deprecated Ordinal.natCast_inj]

theorem Ordinal.nat_cast_inj {m : ℕ} {n : ℕ} : ↑m = ↑n ↔ m = n

Alias of Ordinal.natCast_inj.

@[deprecated Nat.cast_lt]

theorem Ordinal.natCast_lt {m : ℕ} {n : ℕ} : ↑m < ↑n ↔ m < n

@[deprecated Ordinal.natCast_lt]

theorem Ordinal.nat_cast_lt {m : ℕ} {n : ℕ} : ↑m < ↑n ↔ m < n

Alias of Ordinal.natCast_lt.

@[deprecated Nat.cast_eq_zero]

theorem Ordinal.natCast_eq_zero {n : ℕ} : ↑n = 0 ↔ n = 0

@[deprecated Ordinal.natCast_eq_zero]

theorem Ordinal.nat_cast_eq_zero {n : ℕ} : ↑n = 0 ↔ n = 0

Alias of Ordinal.natCast_eq_zero.

@[deprecated Nat.cast_ne_zero]

theorem Ordinal.natCast_ne_zero {n : ℕ} : ↑n ≠ 0 ↔ n ≠ 0

@[deprecated Ordinal.natCast_ne_zero]

theorem Ordinal.nat_cast_ne_zero {n : ℕ} : ↑n ≠ 0 ↔ n ≠ 0

Alias of Ordinal.natCast_ne_zero.

@[deprecated Nat.cast_pos']

theorem Ordinal.natCast_pos {n : ℕ} : 0 < ↑n ↔ 0 < n

@[deprecated Ordinal.natCast_pos]

theorem Ordinal.nat_cast_pos {n : ℕ} : 0 < ↑n ↔ 0 < n

Alias of Ordinal.natCast_pos.

@[simp]

theorem Ordinal.natCast_sub (m : ℕ) (n : ℕ) : ↑(m - n) = ↑m - ↑n

@[deprecated Ordinal.natCast_sub]

theorem Ordinal.nat_cast_sub (m : ℕ) (n : ℕ) : ↑(m - n) = ↑m - ↑n

Alias of Ordinal.natCast_sub.

@[simp]

theorem Ordinal.natCast_div (m : ℕ) (n : ℕ) : ↑(m / n) = ↑m / ↑n

@[deprecated Ordinal.natCast_div]

theorem Ordinal.nat_cast_div (m : ℕ) (n : ℕ) : ↑(m / n) = ↑m / ↑n

Alias of Ordinal.natCast_div.

@[simp]

theorem Ordinal.natCast_mod (m : ℕ) (n : ℕ) : ↑(m % n) = ↑m % ↑n

@[deprecated Ordinal.natCast_mod]

theorem Ordinal.nat_cast_mod (m : ℕ) (n : ℕ) : ↑(m % n) = ↑m % ↑n

Alias of Ordinal.natCast_mod.

@[simp]

theorem Ordinal.lift_natCast (n : ℕ) : Ordinal.lift.{u, v} ↑n = ↑n

@[deprecated Ordinal.lift_natCast]

theorem Ordinal.lift_nat_cast (n : ℕ) : Ordinal.lift.{u, v} ↑n = ↑n

Alias of Ordinal.lift_natCast.

@[simp]

theorem Ordinal.lift_ofNat (n : ℕ) [n.AtLeastTwo] : Ordinal.lift.{u, v} (OfNat.ofNat n) = OfNat.ofNat n

Properties of ω

@[simp]

theorem Cardinal.add_one_of_aleph0_le {c : Cardinal.{u_1}} (h : Cardinal.aleph0 ≤ c) : c + 1 = c

theorem Ordinal.lt_add_of_limit {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} (h : c.IsLimit) : a < b + c ↔ ∃ c' < c, a < b + c'

theorem Ordinal.lt_omega0 {o : Ordinal.{u_1}} : o < Ordinal.omega0 ↔ ∃ (n : ℕ), o = ↑n

@[deprecated Ordinal.lt_omega0]

theorem Ordinal.lt_omega {o : Ordinal.{u_1}} : o < Ordinal.omega0 ↔ ∃ (n : ℕ), o = ↑n

Alias of Ordinal.lt_omega0.

theorem Ordinal.nat_lt_omega0 (n : ℕ) : ↑n < Ordinal.omega0

@[deprecated Ordinal.nat_lt_omega0]

theorem Ordinal.nat_lt_omega (n : ℕ) : ↑n < Ordinal.omega0

Alias of Ordinal.nat_lt_omega0.

theorem Ordinal.omega0_pos : 0 < Ordinal.omega0

@[deprecated]

theorem Ordinal.omega_pos : 0 < Ordinal.omega0

theorem Ordinal.omega0_ne_zero : Ordinal.omega0 ≠ 0

@[deprecated Ordinal.omega0_ne_zero]

theorem Ordinal.omega_ne_zero : Ordinal.omega0 ≠ 0

Alias of Ordinal.omega0_ne_zero.

theorem Ordinal.one_lt_omega0 : 1 < Ordinal.omega0

@[deprecated Ordinal.one_lt_omega0]

theorem Ordinal.one_lt_omega : 1 < Ordinal.omega0

Alias of Ordinal.one_lt_omega0.

theorem Ordinal.isLimit_omega0 : Ordinal.omega0.IsLimit

@[deprecated Ordinal.isLimit_omega0]

theorem Ordinal.omega0_isLimit : Ordinal.omega0.IsLimit

Alias of Ordinal.isLimit_omega0.

@[deprecated Ordinal.isLimit_omega0]

theorem Ordinal.omega_isLimit : Ordinal.omega0.IsLimit

Alias of Ordinal.isLimit_omega0.

theorem Ordinal.omega0_le {o : Ordinal.{u_1}} : Ordinal.omega0 ≤ o ↔ ∀ (n : ℕ), ↑n ≤ o

@[deprecated Ordinal.omega0_le]

theorem Ordinal.omega_le {o : Ordinal.{u_1}} : Ordinal.omega0 ≤ o ↔ ∀ (n : ℕ), ↑n ≤ o

Alias of Ordinal.omega0_le.

@[simp]

theorem Ordinal.iSup_natCast : iSup Nat.cast = Ordinal.omega0

@[deprecated Ordinal.iSup_natCast]

theorem Ordinal.sup_natCast : Ordinal.sup Nat.cast = Ordinal.omega0

@[deprecated Ordinal.sup_natCast]

theorem Ordinal.sup_nat_cast : Ordinal.sup Nat.cast = Ordinal.omega0

Alias of Ordinal.sup_natCast.

theorem Ordinal.nat_lt_limit {o : Ordinal.{u_1}} (h : o.IsLimit) (n : ℕ) : ↑n < o

theorem Ordinal.omega0_le_of_isLimit {o : Ordinal.{u_1}} (h : o.IsLimit) : Ordinal.omega0 ≤ o

@[deprecated Ordinal.omega0_le_of_isLimit]

theorem Ordinal.omega_le_of_isLimit {o : Ordinal.{u_1}} (h : o.IsLimit) : Ordinal.omega0 ≤ o

Alias of Ordinal.omega0_le_of_isLimit.

theorem Ordinal.isLimit_iff_omega0_dvd {a : Ordinal.{u_1}} : a.IsLimit ↔ a ≠ 0 ∧ Ordinal.omega0 ∣ a

@[deprecated Ordinal.isLimit_iff_omega0_dvd]

theorem Ordinal.isLimit_iff_omega_dvd {a : Ordinal.{u_1}} : a.IsLimit ↔ a ≠ 0 ∧ Ordinal.omega0 ∣ a

Alias of Ordinal.isLimit_iff_omega0_dvd.

theorem Ordinal.add_mul_limit_aux {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (ba : b + a = a) (l : c.IsLimit) (IH : ∀ c' < c, (a + b) * Order.succ c' = a * Order.succ c' + b) : (a + b) * c = a * c

theorem Ordinal.add_mul_succ {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (c : Ordinal.{u_1}) (ba : b + a = a) : (a + b) * Order.succ c = a * Order.succ c + b

theorem Ordinal.add_mul_limit {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (ba : b + a = a) (l : c.IsLimit) : (a + b) * c = a * c

theorem Ordinal.add_le_of_forall_add_lt {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (hb : 0 < b) (h : ∀ d < b, a + d < c) : a + b ≤ c

theorem Ordinal.IsNormal.apply_omega0 {f : Ordinal.{u} → Ordinal.{v}} (hf : Ordinal.IsNormal f) : ⨆ (n : ℕ), f ↑n = f Ordinal.omega0

@[deprecated Ordinal.IsNormal.apply_omega0]

theorem Ordinal.IsNormal.apply_omega {f : Ordinal.{u} → Ordinal.{v}} (hf : Ordinal.IsNormal f) : ⨆ (n : ℕ), f ↑n = f Ordinal.omega0

Alias of Ordinal.IsNormal.apply_omega0.

@[simp]

theorem Ordinal.iSup_add_nat (o : Ordinal.{u_1}) : ⨆ (n : ℕ), o + ↑n = o + Ordinal.omega0

@[deprecated Ordinal.iSup_add_nat]

theorem Ordinal.sup_add_nat (o : Ordinal.{u_1}) : (Ordinal.sup fun (n : ℕ) => o + ↑n) = o + Ordinal.omega0

@[simp]

theorem Ordinal.iSup_mul_nat (o : Ordinal.{u_1}) : ⨆ (n : ℕ), o * ↑n = o * Ordinal.omega0

@[deprecated Ordinal.iSup_add_nat]

theorem Ordinal.sup_mul_nat (o : Ordinal.{u_1}) : (Ordinal.sup fun (n : ℕ) => o * ↑n) = o * Ordinal.omega0

theorem Cardinal.isLimit_ord {c : Cardinal.{u_1}} (co : Cardinal.aleph0 ≤ c) : c.ord.IsLimit

@[deprecated Cardinal.isLimit_ord]

theorem Cardinal.ord_isLimit {c : Cardinal.{u_1}} (co : Cardinal.aleph0 ≤ c) : c.ord.IsLimit

Alias of Cardinal.isLimit_ord.

theorem Cardinal.noMaxOrder {c : Cardinal.{u_1}} (h : Cardinal.aleph0 ≤ c) : NoMaxOrder c.ord.toType