# Arithmetic on families of ordinals #

## Main definitions and results #

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

### Families of ordinals #

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

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

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

Instances For

source
def Ordinal.bfamilyOfFamily {α : Type u_1} {ι : Type u} :
(ι → α) → (a : Ordinal.{u}) → a < 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

Instances For

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

Instances For

source
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

Instances For

source
@[simp]
theorem Ordinal.bfamilyOfFamily'_typein {α : Type u_1} {ι : Type u_4} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (i : ι) :
bfamilyOfFamily' r f ((typein r).toRelEmbedding i) ⋯ = f i
source
@[simp]
theorem Ordinal.bfamilyOfFamily_typein {α : Type u_1} {ι : Type u_4} (f : ι → α) (i : ι) :
bfamilyOfFamily f ((typein WellOrderingRel).toRelEmbedding i) ⋯ = f i
source
theorem Ordinal.familyOfBFamily'_enum {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : type r = o) (f : (a : Ordinal.{u}) → a < o → α) (i : Ordinal.{u}) (hi : i < o) :
familyOfBFamily' r ho f ((enum r) ⟨i, ⋯⟩) = f i hi
source
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 ((enum fun (x1 x2 : o.toType) => x1 < x2) ⟨i, ⋯⟩) = f i hi
source
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.7}) (hi : i < o), f i hi = a}

Instances For

source
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
source
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
source
@[simp]
theorem Ordinal.range_familyOfBFamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : type r = o) (f : (a : Ordinal.{u}) → a < o → α) :
Set.range (familyOfBFamily' r ho f) = o.brange f
source
@[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
source
@[simp]
theorem Ordinal.brange_bfamilyOfFamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) :
(type r).brange (bfamilyOfFamily' r f) = Set.range f
source
@[simp]
theorem Ordinal.brange_bfamilyOfFamily {α : Type u_1} {ι : Type u} (f : ι → α) :
(type WellOrderingRel).brange (bfamilyOfFamily f) = Set.range f
source
@[simp]
theorem Ordinal.brange_const {α : Type u_1} {o : Ordinal.{u_4}} (ho : o ≠ 0) {c : α} :
(o.brange fun (x : Ordinal.{u_4}) (x_1 : x < o) => c) = {c}
source
theorem Ordinal.comp_bfamilyOfFamily' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (g : α → β) :
(fun (i : Ordinal.{u}) (hi : i < type r) => g (bfamilyOfFamily' r f i hi)) = bfamilyOfFamily' r (g ∘ f)
source
theorem Ordinal.comp_bfamilyOfFamily {α : Type u_1} {β : Type u_2} {ι : Type u} (f : ι → α) (g : α → β) :
(fun (i : Ordinal.{u}) (hi : i < type WellOrderingRel) => g (bfamilyOfFamily f i hi)) = bfamilyOfFamily (g ∘ f)
source
theorem Ordinal.comp_familyOfBFamily' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : type r = o) (f : (a : Ordinal.{u}) → a < o → α) (g : α → β) :
g ∘ familyOfBFamily' r ho f = familyOfBFamily' r ho fun (i : Ordinal.{u}) (hi : i < o) => g (f i hi)
source
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 #

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

source
theorem Ordinal.bddAbove_of_small (s : Set Ordinal.{u}) [h : Small.{u, u + 1} ↑s] :
BddAbove s
source
theorem Ordinal.bddAbove_iff_small {s : Set Ordinal.{u}} :
BddAbove s ↔ Small.{u, u + 1} ↑s
source
theorem Ordinal.bddAbove_image {s : Set Ordinal.{u}} (hf : BddAbove s) (f : Ordinal.{u} → Ordinal.{max u v}) :
BddAbove (f '' s)
source
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))
source
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.

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

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

source
theorem Ordinal.lt_iSup_iff {ι : 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.

source
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
source
theorem Ordinal.iSup_eq_zero_iff {ι : Type u_4} {f : ι → Ordinal.{u}} [Small.{u, u_4} ι] :
iSup f = 0 ↔ ∀ (i : ι), f i = 0
source
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
source
@[deprecated iSup_succ (since := "2025-10-08")]
theorem Ordinal.iSup_succ {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] [SuccOrder α] (x : α) :
⨆ (a : ↑(Set.Iio x)), Order.succ ↑a = x

Alias of `iSup_succ`.

source
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))
source
theorem Ordinal.unbounded_range_of_le_iSup {α β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β → α) (h : type r ≤ ⨆ (i : β), (typein r).toRelEmbedding (f i)) :
Set.Unbounded r (Set.range f)
source
theorem Ordinal.IsNormal.map_iSup_of_bddAbove {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {ι : Type u_4} (g : ι → Ordinal.{u}) (hg : BddAbove (Set.range g)) [Nonempty ι] :
f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
source
theorem Ordinal.IsNormal.map_iSup {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {ι : Type w} (g : ι → Ordinal.{u}) [Small.{u, w} ι] [Nonempty ι] :
f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
source
theorem Ordinal.IsNormal.map_sSup_of_bddAbove {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {s : Set Ordinal.{u}} (hs : BddAbove s) (hn : s.Nonempty) :
f (sSup s) = sSup (f '' s)
source
theorem Ordinal.IsNormal.map_sSup {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {s : Set Ordinal.{u}} (hn : s.Nonempty) [Small.{u, u + 1} ↑s] :
f (sSup s) = sSup (f '' s)
source
theorem Ordinal.IsNormal.apply_of_isSuccLimit {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {o : Ordinal.{u}} (ho : Order.IsSuccLimit o) :
f o = ⨆ (a : ↑(Set.Iio o)), f ↑a
source
@[deprecated Ordinal.IsNormal.apply_of_isSuccLimit (since := "2025-07-08")]
theorem Ordinal.IsNormal.apply_of_isLimit {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {o : Ordinal.{u}} (ho : Order.IsSuccLimit o) :
f o = ⨆ (a : ↑(Set.Iio o)), f ↑a

Alias of `Ordinal.IsNormal.apply_of_isSuccLimit`.

source
theorem Ordinal.sSup_ord (s : Set Cardinal.{u_4}) :
(sSup s).ord = sSup (Cardinal.ord '' s)
source
theorem Ordinal.iSup_ord {ι : Sort u_4} (f : ι → Cardinal.{u_5}) :
(⨆ (i : ι), f i).ord = ⨆ (i : ι), (f i).ord
source
theorem Ordinal.lift_card_sInf_compl_le (s : Set Ordinal.{u}) :
Cardinal.lift.{u + 1, u} (sInf s ᶜ).card ≤ Cardinal.mk ↑s
source
theorem Ordinal.card_sInf_range_compl_le_lift {ι : Type u} (f : ι → Ordinal.{max u v}) :
(sInf (Set.range f)ᶜ).card ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)
source
theorem Ordinal.card_sInf_range_compl_le {ι : Type u} (f : ι → Ordinal.{u}) :
(sInf (Set.range f)ᶜ).card ≤ Cardinal.mk ι
source
theorem Ordinal.sInf_compl_lt_lift_ord_succ {ι : Type u} (f : ι → Ordinal.{max u v}) :
sInf (Set.range f)ᶜ < lift.{v, u} (Order.succ (Cardinal.mk ι)).ord
source
theorem Ordinal.sInf_compl_lt_ord_succ {ι : Type u} (f : ι → Ordinal.{u}) :
sInf (Set.range f)ᶜ < (Order.succ (Cardinal.mk ι)).ord
source
theorem Ordinal.iSup_eq_iSup {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : type r = o) (ho' : type r' = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u_4}) :
iSup (familyOfBFamily' r ho f) = iSup (familyOfBFamily' r' ho' f)
source
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 `iSup` over the family provided by `familyOfBFamily`.

Equations

- o.bsup f = iSup (o.familyOfBFamily f)

Instances For

source
@[simp]
theorem Ordinal.iSup_eq_bsup {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}) :
iSup (o.familyOfBFamily f) = o.bsup f
source
theorem Ordinal.iSup'_eq_bsup {o : Ordinal.{u_4}} {ι : Type u_4} (r : ι → ι → Prop) [IsWellOrder ι r] (ho : type r = o) (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}) :
iSup (familyOfBFamily' r ho f) = o.bsup f
source
theorem Ordinal.sSup_eq_bsup {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}) :
sSup (o.brange f) = o.bsup f
source
@[simp]
theorem Ordinal.bsup'_eq_iSup {ι : Type u_4} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u_4 u_5}) :
(type r).bsup (bfamilyOfFamily' r f) = iSup f
source
@[simp]
theorem Ordinal.bsup_eq_iSup {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
(type WellOrderingRel).bsup (bfamilyOfFamily f) = iSup f
source
theorem Ordinal.bsup_eq_bsup {ι : Type u} (r r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r'] (f : ι → Ordinal.{max u v}) :
(type r).bsup (bfamilyOfFamily' r f) = (type r').bsup (bfamilyOfFamily' r' f)
source
theorem Ordinal.bsup_congr {o₁ 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 ⋯
source
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
source
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
source
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
source
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
source
theorem Ordinal.IsNormal.bsup {f : Ordinal.{max u_4 u_5} → Ordinal.{max u_5 u_6}} (H : IsNormal f) {o : Ordinal.{u_5}} (g : (a : Ordinal.{u_5}) → a < o → Ordinal.{max u_5 u_4}) :
o ≠ 0 → f (o.bsup g) = o.bsup fun (a : Ordinal.{u_5}) (h : a < o) => f (g a h)
source
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
source
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
source
@[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
source
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
source
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 ⋯
source
@[simp]
theorem Ordinal.bsup_zero (f : (a : Ordinal.{u_4}) → a < 0 → Ordinal.{max u_4 u_5}) :
bsup 0 f = 0
source
theorem Ordinal.bsup_const {o : Ordinal.{u}} (ho : o ≠ 0) (a : Ordinal.{max u v}) :
(o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => a) = a
source
@[simp]
theorem Ordinal.bsup_one (f : (a : Ordinal.{u_4}) → a < 1 → Ordinal.{max u_4 u_5}) :
bsup 1 f = f 0 ⋯
source
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
source
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
source
theorem Ordinal.iSup_Iio_eq_bsup {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}} :
⨆ (a : ↑(Set.Iio o)), f ↑a ⋯ = o.bsup f
source
@[deprecated Ordinal.iSup_eq_iSup (since := "2025-10-01")]
theorem Ordinal.sup_eq_sup {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : type r = o) (ho' : type r' = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u_4}) :
iSup (familyOfBFamily' r ho f) = iSup (familyOfBFamily' r' ho' f)

Alias of `Ordinal.iSup_eq_iSup`.

source
@[deprecated Ordinal.iSup'_eq_bsup (since := "2025-10-01")]
theorem Ordinal.sup_eq_bsup' {o : Ordinal.{u_4}} {ι : Type u_4} (r : ι → ι → Prop) [IsWellOrder ι r] (ho : type r = o) (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}) :
iSup (familyOfBFamily' r ho f) = o.bsup f

Alias of `Ordinal.iSup'_eq_bsup`.

source
@[deprecated Ordinal.iSup_eq_bsup (since := "2025-10-01")]
theorem Ordinal.sup_eq_bsup {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}) :
iSup (o.familyOfBFamily f) = o.bsup f

Alias of `Ordinal.iSup_eq_bsup`.

source
@[deprecated Ordinal.bsup'_eq_iSup (since := "2025-10-01")]
theorem Ordinal.bsup_eq_sup' {ι : Type u_4} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u_4 u_5}) :
(type r).bsup (bfamilyOfFamily' r f) = iSup f

Alias of `Ordinal.bsup'_eq_iSup`.

source
@[deprecated Ordinal.bsup_eq_iSup (since := "2025-10-01")]
theorem Ordinal.bsup_eq_sup {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
(type WellOrderingRel).bsup (bfamilyOfFamily f) = iSup f

Alias of `Ordinal.bsup_eq_iSup`.

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

The least strict upper bound of a family of ordinals.

Equations

- Ordinal.lsub f = iSup (Order.succ ∘ f)

Instances For

source
@[simp]
theorem Ordinal.iSup_eq_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
iSup (Order.succ ∘ f) = lsub f
source
theorem Ordinal.lsub_le_iff {ι : Type u_4} {f : ι → Ordinal.{max u_5 u_4}} {a : Ordinal.{max u_4 u_5}} :
lsub f ≤ a ↔ ∀ (i : ι), f i < a
source
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) → lsub f ≤ a
source
theorem Ordinal.lt_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) (i : ι) :
f i < lsub f
source
theorem Ordinal.lt_lsub_iff {ι : Type u_4} {f : ι → Ordinal.{max u_5 u_4}} {a : Ordinal.{max u_4 u_5}} :
a < lsub f ↔ ∃ (i : ι), a ≤ f i
source
theorem Ordinal.iSup_le_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
iSup f ≤ lsub f
source
theorem Ordinal.lsub_le_succ_iSup {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
lsub f ≤ Order.succ (iSup f)
source
theorem Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
iSup f = lsub f ∨ Order.succ (iSup f) = lsub f
source
theorem Ordinal.succ_iSup_le_lsub_iff {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
Order.succ (iSup f) ≤ lsub f ↔ ∃ (i : ι), f i = iSup f
source
theorem Ordinal.succ_iSup_eq_lsub_iff {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
Order.succ (iSup f) = lsub f ↔ ∃ (i : ι), f i = iSup f
source
theorem Ordinal.iSup_eq_lsub_iff {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
iSup f = lsub f ↔ ∀ a < lsub f, Order.succ a < lsub f
source
theorem Ordinal.iSup_eq_lsub_iff_lt_iSup {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
iSup f = lsub f ↔ ∀ (i : ι), f i < iSup f
source
@[simp]
theorem Ordinal.lsub_empty {ι : Type u_4} [h : IsEmpty ι] (f : ι → Ordinal.{max u_5 u_4}) :
lsub f = 0
source
theorem Ordinal.lsub_pos {ι : Type u_4} [h : Nonempty ι] (f : ι → Ordinal.{max u_5 u_4}) :
0 < lsub f
source
@[simp]
theorem Ordinal.lsub_eq_zero_iff {ι : Type u_4} (f : ι → Ordinal.{max v u_4}) :
lsub f = 0 ↔ IsEmpty ι
source
@[simp]
theorem Ordinal.lsub_const {ι : Type u_4} [Nonempty ι] (o : Ordinal.{max u_5 u_4}) :
(lsub fun (x : ι) => o) = Order.succ o
source
@[simp]
theorem Ordinal.lsub_unique {ι : Type u_4} [Unique ι] (f : ι → Ordinal.{max u_5 u_4}) :
lsub f = Order.succ (f default)
source
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) :
lsub f ≤ lsub g
source
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) :
lsub f = lsub g
source
@[simp]
theorem Ordinal.lsub_sum {α : Type u} {β : Type v} (f : α ⊕ β → Ordinal.{max (max u v) w}) :
lsub f = max (lsub fun (a : α) => f (Sum.inl a)) (lsub fun (b : β) => f (Sum.inr b))
source
theorem Ordinal.lsub_notMem_range {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
lsub f ∉ Set.range f
source
@[deprecated Ordinal.lsub_notMem_range (since := "2025-05-23")]
theorem Ordinal.lsub_not_mem_range {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
lsub f ∉ Set.range f

Alias of `Ordinal.lsub_notMem_range`.

source
theorem Ordinal.nonempty_compl_range {ι : Type u} (f : ι → Ordinal.{max u v}) :
(Set.range f)ᶜ.Nonempty
source
@[simp]
theorem Ordinal.lsub_typein (o : Ordinal.{u}) :
lsub ⇑(typein fun (x1 x2 : o.toType) => x1 < x2).toRelEmbedding = o
source
theorem Ordinal.iSup_typein_limit {o : Ordinal.{u}} (ho : ∀ a < o, Order.succ a < o) :
iSup ⇑(typein fun (x1 x2 : o.toType) => x1 < x2).toRelEmbedding = o
source
@[simp]
theorem Ordinal.iSup_typein_succ {o : Ordinal.{u_4}} :
iSup ⇑(typein fun (x1 x2 : (Order.succ o).toType) => x1 < x2).toRelEmbedding = o
source
@[deprecated Ordinal.iSup_eq_lsub (since := "2025-10-01")]
theorem Ordinal.sup_eq_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
iSup (Order.succ ∘ f) = lsub f

Alias of `Ordinal.iSup_eq_lsub`.

source
@[deprecated Ordinal.iSup_le_lsub (since := "2025-10-01")]
theorem Ordinal.sup_le_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
iSup f ≤ lsub f

Alias of `Ordinal.iSup_le_lsub`.

source
@[deprecated Ordinal.lsub_le_succ_iSup (since := "2025-10-01")]
theorem Ordinal.lsub_le_sup_succ {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
lsub f ≤ Order.succ (iSup f)

Alias of `Ordinal.lsub_le_succ_iSup`.

source
@[deprecated Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub (since := "2025-10-01")]
theorem Ordinal.sup_eq_lsub_or_sup_succ_eq_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
iSup f = lsub f ∨ Order.succ (iSup f) = lsub f

Alias of `Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub`.

source
@[deprecated Ordinal.succ_iSup_le_lsub_iff (since := "2025-10-01")]
theorem Ordinal.sup_succ_le_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
Order.succ (iSup f) ≤ lsub f ↔ ∃ (i : ι), f i = iSup f

Alias of `Ordinal.succ_iSup_le_lsub_iff`.

source
@[deprecated Ordinal.succ_iSup_eq_lsub_iff (since := "2025-10-01")]
theorem Ordinal.sup_succ_eq_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
Order.succ (iSup f) = lsub f ↔ ∃ (i : ι), f i = iSup f

Alias of `Ordinal.succ_iSup_eq_lsub_iff`.

source
@[deprecated Ordinal.iSup_eq_lsub_iff (since := "2025-10-01")]
theorem Ordinal.sup_eq_lsub_iff_succ {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
iSup f = lsub f ↔ ∀ a < lsub f, Order.succ a < lsub f

Alias of `Ordinal.iSup_eq_lsub_iff`.

source
@[deprecated Ordinal.iSup_eq_lsub_iff_lt_iSup (since := "2025-10-01")]
theorem Ordinal.sup_eq_lsub_iff_lt_sup {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :
iSup f = lsub f ↔ ∀ (i : ι), f i < iSup f

Alias of `Ordinal.iSup_eq_lsub_iff_lt_iSup`.

source
@[deprecated Ordinal.iSup_typein_limit (since := "2025-10-01")]
theorem Ordinal.sup_typein_limit {o : Ordinal.{u}} (ho : ∀ a < o, Order.succ a < o) :
iSup ⇑(typein fun (x1 x2 : o.toType) => x1 < x2).toRelEmbedding = o

Alias of `Ordinal.iSup_typein_limit`.

source
@[deprecated Ordinal.iSup_typein_succ (since := "2025-10-01")]
theorem Ordinal.sup_typein_succ {o : Ordinal.{u_4}} :
iSup ⇑(typein fun (x1 x2 : (Order.succ o).toType) => x1 < x2).toRelEmbedding = o

Alias of `Ordinal.iSup_typein_succ`.

source
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.22}) (ha : a < o) => Order.succ (f a ha)

Instances For

source
@[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
source
theorem Ordinal.lsub_eq_blsub' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : type r = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u u_4}) :
lsub (familyOfBFamily' r ho f) = o.blsub f
source
theorem Ordinal.lsub_eq_lsub {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : type r = o) (ho' : type r' = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) :
lsub (familyOfBFamily' r ho f) = lsub (familyOfBFamily' r' ho' f)
source
@[simp]
theorem Ordinal.lsub_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) :
lsub (o.familyOfBFamily f) = o.blsub f
source
@[simp]
theorem Ordinal.blsub_eq_lsub' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u v}) :
(type r).blsub (bfamilyOfFamily' r f) = lsub f
source
theorem Ordinal.blsub_eq_blsub {ι : Type u} (r r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r'] (f : ι → Ordinal.{max u v}) :
(type r).blsub (bfamilyOfFamily' r f) = (type r').blsub (bfamilyOfFamily' r' f)
source
@[simp]
theorem Ordinal.blsub_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) :
(type WellOrderingRel).blsub (bfamilyOfFamily f) = lsub f
source
theorem Ordinal.blsub_congr {o₁ 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 ⋯
source
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
source
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
source
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
source
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
source
theorem Ordinal.bsup_le_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) :
o.bsup f ≤ o.blsub f
source
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)
source
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
source
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
source
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
source
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
source
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
source
theorem Ordinal.bsup_eq_blsub_of_lt_succ_limit {o : Ordinal.{u}} (ho : Order.IsSuccLimit o) {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
source
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 ⋯)
source
@[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
source
@[simp]
theorem Ordinal.blsub_zero (f : (a : Ordinal.{u_4}) → a < 0 → Ordinal.{max u_4 u_5}) :
blsub 0 f = 0
source
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
source
theorem Ordinal.blsub_type {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}) :
(type r).blsub f = lsub fun (a : α) => f ((typein r).toRelEmbedding a) ⋯
source
theorem Ordinal.blsub_const {o : Ordinal.{u}} (ho : o ≠ 0) (a : Ordinal.{max u v}) :
(o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => a) = Order.succ a
source
@[simp]
theorem Ordinal.blsub_one (f : (a : Ordinal.{u_4}) → a < 1 → Ordinal.{max u_4 u_5}) :
blsub 1 f = Order.succ (f 0 ⋯)
source
@[simp]
theorem Ordinal.blsub_id (o : Ordinal.{u}) :
(o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => x) = o
source
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
source
@[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
source
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
source
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
source
theorem Ordinal.bsup_comp {o 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
source
theorem Ordinal.blsub_comp {o 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
source
theorem Ordinal.IsNormal.bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}} (H : IsNormal f) {o : Ordinal.{u}} (h : Order.IsSuccLimit o) :
(o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o
source
theorem Ordinal.IsNormal.blsub_eq {f : Ordinal.{u} → Ordinal.{max u v}} (H : IsNormal f) {o : Ordinal.{u}} (h : Order.IsSuccLimit o) :
(o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o
source
theorem Ordinal.isNormal_iff_lt_succ_and_bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}} :
IsNormal f ↔ (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧ ∀ (o : Ordinal.{u}), Order.IsSuccLimit o → (o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o
source
theorem Ordinal.isNormal_iff_lt_succ_and_blsub_eq {f : Ordinal.{u} → Ordinal.{max u v}} :
IsNormal f ↔ (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧ ∀ (o : Ordinal.{u}), Order.IsSuccLimit o → (o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o
source
theorem Ordinal.IsNormal.eq_iff_zero_and_succ {f g : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (hg : IsNormal g) :
f = g ↔ f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (Order.succ a) = g (Order.succ a)

### Results about injectivity and surjectivity #

source
theorem not_surjective_of_ordinal {α : Type u_1} [Small.{u, u_1} α] (f : α → Ordinal.{u}) :
¬Function.Surjective f
source
theorem not_injective_of_ordinal {α : Type u_1} [Small.{u, u_1} α] (f : Ordinal.{u} → α) :
¬Function.Injective f
source
@[deprecated not_surjective_of_ordinal (since := "2025-08-21")]
theorem not_surjective_of_ordinal_of_small {α : Type u_1} [Small.{u, u_1} α] (f : α → Ordinal.{u}) :
¬Function.Surjective f

Alias of `not_surjective_of_ordinal`.

source
@[deprecated not_injective_of_ordinal (since := "2025-08-21")]
theorem not_injective_of_ordinal_of_small {α : Type u_1} [Small.{u, u_1} α] (f : Ordinal.{u} → α) :
¬Function.Injective f

Alias of `not_injective_of_ordinal`.

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

source
instance Ordinal.uncountable :
Uncountable Ordinal.{u}
source
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 #

source
@[simp]
theorem Ordinal.iSup_natCast :
iSup Nat.cast = omega0
source
theorem Ordinal.IsNormal.apply_omega0 {f : Ordinal.{u} → Ordinal.{v}} (hf : IsNormal f) :
⨆ (n : ℕ), f ↑n = f omega0
source
@[simp]
theorem Ordinal.iSup_add_nat (o : Ordinal.{u_1}) :
⨆ (n : ℕ), o + ↑n = o + omega0
source
@[simp]
theorem Ordinal.iSup_mul_nat (o : Ordinal.{u_1}) :
⨆ (n : ℕ), o * ↑n = o * omega0